src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43915 ef347714c5c1
parent 43911 a1da544e2652
child 44241 7943b69f0188
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Jul 20 08:16:39 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Jul 20 08:16:41 2011 +0200
@@ -285,9 +285,9 @@
             end 
       in with_size 0 end
   in
-    Quickcheck.limit timeout (limit_time, is_interactive) 
-      (fn () => with_tmp_dir tmp_prefix run)
-      (fn () => (message (excipit ()); (NONE, !current_result))) ()
+    (*Quickcheck.limit timeout (limit_time, is_interactive) 
+      (fn () =>*) with_tmp_dir tmp_prefix run
+      (*(fn () => (message (excipit ()); (NONE, !current_result))) ()*)
   end;
 
 fun dynamic_value_strict opts cookie thy postproc t =