load theory explicitly
authorhaftmann
Fri, 24 Sep 2010 11:56:14 +0200
changeset 39674 dacf4bad3954
parent 39668 9d554d257a10
child 39675 b4cbc72a354c
load theory explicitly
src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Thu Sep 23 21:17:11 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Fri Sep 24 11:56:14 2010 +0200
@@ -50,7 +50,7 @@
 
 ## invoke code generation
 
-FORMAL_CMD="Toplevel.program (fn () => ML_Context.eval_text_in \
+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) \
   handle _ => OS.Process.exit OS.Process.failure;"