src/Tools/quickcheck.ML

   val add_report : int -> report option -> result Unsynchronized.ref -> unit
   val counterexample_of : result -> (string * term) list option
   val timings_of : result -> (string * int) list
   (* registering testers & generators *) 
   type tester =
-    Proof.context -> (string * typ) list -> (term * term list) list -> result list
+    Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list
   val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic
   val add_batch_generator :
     string * (Proof.context -> term list -> (int -> term list option) list)
       -> Context.generic -> Context.generic
   val add_batch_validator :

     Test_Params {default_type = default_type2, expect = expect2}) =
   make_test_params
     (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
 
 type tester =
-  Proof.context -> (string * typ) list -> (term * term list) list -> result list
+  Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list
 
 structure Data = Generic_Data
 (
   type T =
     ((string * (bool Config.T * tester)) list

 fun test_terms ctxt (limit_time, is_interactive) insts goals =
   case active_testers ctxt of
     [] => error "No active testers for quickcheck"
   | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
       (fn () => Par_List.get_some (fn tester =>
-      tester ctxt insts goals |>
+      tester ctxt (length testers > 1) insts goals |>
       (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
       (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ();
       
 fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
   let