diff -r e5ef7aa77fde -r 10ba32c347b0 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Nov 09 11:34:57 2011 +0100
+++ b/src/Tools/quickcheck.ML	Wed Nov 09 11:34:59 2011 +0100
@@ -50,7 +50,7 @@
   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)
@@ -192,7 +192,7 @@
     (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
 (
@@ -288,7 +288,7 @@
     [] => 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)) ();