diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 59fbf566c0d..ced036cd1e0 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -396,7 +396,8 @@ bool AletheProofPostprocessCallback::update(Node res,
       if (rewriter::getDslProofRule(args[0], di))
       {
         std::stringstream ss;
-        ss << "\"" << di << "\"";
+        //ss << "\"" << di << "\"";
+        ss << di;
         rule = nm->mkRawSymbol(ss.str(), nm->sExprType());
       }
       else
@@ -437,7 +438,8 @@ bool AletheProofPostprocessCallback::update(Node res,
                            res,
                            nm->mkNode(Kind::SEXPR, d_cl, res),
                            children,
-                           {nm->mkRawSymbol("\"arith-poly-norm\"", nm->sExprType())},
+                           {nm->mkRawSymbol("arith-poly-norm", nm->sExprType())},
+                           //{nm->mkRawSymbol("\"arith-poly-norm\"", nm->sExprType())},
                            *cdp);
     }
     case ProofRule::EVALUATE:
@@ -446,7 +448,8 @@ bool AletheProofPostprocessCallback::update(Node res,
                            res,
                            nm->mkNode(Kind::SEXPR, d_cl, res),
                            children,
-                           {nm->mkRawSymbol("\"evaluate\"", nm->sExprType())},
+                           {nm->mkRawSymbol("evaluate", nm->sExprType())},
+                           //{nm->mkRawSymbol("\"evaluate\"", nm->sExprType())},
                            *cdp);
     }
     case ProofRule::TRUST_THEORY_REWRITE: