diff -r f99ec71de82d -r 323f7aad54b0 src/Tools/Code/code_runtime.ML
--- 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