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