# HG changeset patch
# User wenzelm
# Date 1307564181 -7200
# Node ID 10d731b06ed7761165e258d789598494bd6bd027
# Parent  c835416237b392a80e87f8babdef09fe302c3ae6
modernized structure ProofContext;

diff -r c835416237b3 -r 10d731b06ed7 src/Tools/Code/lib/Tools/codegen
--- 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\"; \