less verbosity -- do not print final ();
authorwenzelm
Thu, 30 May 2013 22:26:16 +0200
changeset 52263 320c86e50f84
parent 52262 f22d227a090c
child 52264 cdba0c3cb4c2
less verbosity -- do not print final ();
src/HOL/Spec_Check/spec_check.ML
--- a/src/HOL/Spec_Check/spec_check.ML	Thu May 30 22:16:33 2013 +0200
+++ b/src/HOL/Spec_Check/spec_check.ML	Thu May 30 22:26:16 2013 +0200
@@ -143,7 +143,7 @@
 (*call the compiler and run the test*)
 fun run_test ctxt s =
   Context.setmp_thread_data (SOME (Context.Proof ctxt))
-    (fn () => Secure.use_text ML_Env.local_context (0, "generated code") true s) ();
+    (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
 
 (*split input into tokens*)
 fun input_split s =