minor fix

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index dc85d0cd672fef20b2573980455afd84bff030bc..389bcca8b23bb260ccdb267c1714b99822a58f88 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -266,7 +266,7 @@ public:
         if( dt.isParametric() ){
           tn = TypeNode::fromType( tspec )[i];
         }
-        nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created for inst cons" );
+        nc = NodeManager::currentNM()->mkSkolem( "m", tn, "created for inst cons" );
       }
       children.push_back( nc );
     }