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