author | wenzelm |
Sun, 07 Jan 2001 21:36:59 +0100 | |
changeset 10818 | 37fa05a12459 |
parent 10817 | 083d4a6734b4 |
child 10819 | 4e056473ae30 |
--- 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 _ _ _ [] = []