# HG changeset patch
# User wenzelm
# Date 1511779520 -3600
# Node ID e77f13a6a50107ddb51bc5e3e7eb1bd3ded17791
# Parent  91ffe1f8bf5c1a947f27cf0a14358171ab53fb23
proper context (as in 'term' command);

diff -r 91ffe1f8bf5c -r e77f13a6a501 src/HOL/ex/Commands.thy
--- 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