tuned output;
authorwenzelm
Sun, 07 Jan 2001 21:36:59 +0100
changeset 10818 37fa05a12459
parent 10817 083d4a6734b4
child 10819 4e056473ae30
tuned output;
src/Pure/Isar/proof_context.ML
--- 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 _ _ _ [] = []