changeset 67096 | e77f13a6a501 |
parent 59936 | b8ffc3dc9e24 |
child 69597 | ff784d5a5bfb |
--- 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