# HG changeset patch
# User haftmann
# Date 1285322174 -7200
# Node ID dacf4bad3954ad46ced98e3754892a15720c11ed
# Parent  9d554d257a1075107d4fb0d6ad87a671e1db1daf
load theory explicitly

diff -r 9d554d257a10 -r dacf4bad3954 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;"