# HG changeset patch
# User haftmann
# Date 1285322184 -7200
# Node ID b4cbc72a354cc8fef2b2b3bc109e49123d0a7c07
# Parent  fabd6b48fe6e887e94b2068f908c90a492724061# Parent  dacf4bad3954ad46ced98e3754892a15720c11ed
merged

diff -r fabd6b48fe6e -r b4cbc72a354c src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Fri Sep 24 11:36:28 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Fri Sep 24 11:56:24 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;"