# HG changeset patch
# User wenzelm
# Date 1369945576 -7200
# Node ID 320c86e50f84820f4c5d72d32a479ec6a4499a8f
# Parent  f22d227a090c5459c9cd387d0775e9edcf963594
less verbosity -- do not print final ();

diff -r f22d227a090c -r 320c86e50f84 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 =