1.1 --- a/src/Tools/quickcheck.ML	Mon Oct 25 21:17:10 2010 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Mon Oct 25 21:17:11 2010 +0200
     1.3 @@ -194,10 +194,12 @@
     1.4            val (result, new_report) = with_testers k testers
     1.5            val reports = ((k, new_report) :: reports)
     1.6          in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
     1.7 -    val ((result, reports), exec_time) = cpu_time "quickcheck execution"
     1.8 +    val ((result, reports), exec_time) =
     1.9 +      TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => cpu_time "quickcheck execution"
    1.10        (fn () => apfst
    1.11           (fn result => case result of NONE => NONE
    1.12 -        | SOME ts => SOME (names ~~ ts)) (with_size 1 []))
    1.13 +        | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
    1.14 +      handle TimeLimit.TimeOut => error "Reached timeout during Quickcheck"
    1.15    in
    1.16      (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
    1.17    end;