src/Tools/Code/code_runtime.ML
changeset 40257 323f7aad54b0
parent 40235 87998864284e
child 40320 abc52faa7761
--- a/src/Tools/Code/code_runtime.ML	Fri Oct 29 11:07:21 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Oct 29 11:35:28 2010 +0200
@@ -64,7 +64,7 @@
 
 fun exec verbose code =
   (if ! trace then tracing code else ();
-  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false code));
+  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
   let