1.1 --- a/src/Tools/quickcheck.ML	Wed Nov 09 11:34:55 2011 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Wed Nov 09 11:34:57 2011 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4    val timings_of : result -> (string * int) list
     1.5    (* registering testers & generators *) 
     1.6    type tester =
     1.7 -    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
     1.8 +    Proof.context -> (string * typ) list -> (term * term list) list -> result list
     1.9    val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic
    1.10    val add_batch_generator :
    1.11      string * (Proof.context -> term list -> (int -> term list option) list)
    1.12 @@ -192,7 +192,7 @@
    1.13      (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
    1.14  
    1.15  type tester =
    1.16 -  Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
    1.17 +  Proof.context -> (string * typ) list -> (term * term list) list -> result list
    1.18  
    1.19  structure Data = Generic_Data
    1.20  (
    1.21 @@ -288,7 +288,7 @@
    1.22      [] => error "No active testers for quickcheck"
    1.23    | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
    1.24        (fn () => Par_List.get_some (fn tester =>
    1.25 -      tester ctxt (limit_time, is_interactive) insts goals |>
    1.26 +      tester ctxt insts goals |>
    1.27        (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
    1.28        (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ();
    1.29