--- 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"