--- a/src/Tools/Code/lib/Tools/codegen Thu Jun 09 17:58:42 2011 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Wed Jun 08 22:16:21 2011 +0200
@@ -51,7 +51,7 @@
## invoke code generation
FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
- (SOME (ProofContext.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
+ (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
handle _ => OS.Process.exit OS.Process.failure;"
ACTUAL_CMD="val thyname = \"$THYNAME\"; \