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 _ _ _ [] = []