# HG changeset patch
# User wenzelm
# Date 978899819 -3600
# Node ID 37fa05a12459b796c412f66930923a3771c549c9
# Parent  083d4a6734b4e3efce90468edca67feecbb2e95c
tuned output;

diff -r 083d4a6734b4 -r 37fa05a12459 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 _ _ _ [] = []