src/Pure/Isar/proof_context.ML
changeset 10818 37fa05a12459
parent 10810 619586bd854b
child 10830 d19f9f4c35ee
--- a/src/Pure/Isar/proof_context.ML	Sun Jan 07 21:36:11 2001 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Jan 07 21:36:59 2001 +0100
@@ -1029,7 +1029,7 @@
   let
     val prt_term = Sign.pretty_term (sign_of ctxt);
     fun prt_let (xi, t) = Pretty.block
-      [prt_term (Var (xi, Term.fastype_of t)), Pretty.str " =", Pretty.brk 1,
+      [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
         Pretty.quote (prt_term t)];
 
     fun prt_sect _ _ _ [] = []