ProofContext.init_global
authorhaftmann
Thu, 06 May 2010 10:55:09 +0200
changeset 36694 978e6469b504
parent 36693 40dcc319d4cd
child 36695 b434506fb0d4
child 36717 2a72455be88b
ProofContext.init_global
src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Thu May 06 08:44:19 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Thu May 06 10:55:09 2010 +0200
@@ -58,7 +58,7 @@
   QND_CMD="reset"
 fi
 
-CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
 
 FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"