author | wenzelm |
Mon, 27 Nov 2017 11:45:20 +0100 | |
changeset 67096 | e77f13a6a501 |
parent 67095 | 91ffe1f8bf5c |
child 67097 | d1b8464654c5 |
--- a/src/HOL/ex/Commands.thy Mon Nov 27 11:40:41 2017 +0100 +++ b/src/HOL/ex/Commands.thy Mon Nov 27 11:45:20 2017 +0100 @@ -20,7 +20,8 @@ let val ctxt = Toplevel.context_of st; val t = Syntax.read_term ctxt s; - in Pretty.writeln (Syntax.pretty_term ctxt t) end))); + val ctxt' = Variable.auto_fixes t ctxt; + in Pretty.writeln (Syntax.pretty_term ctxt' t) end))); \<close> print_test x