diff -r 8f176e575a49 -r 0c47d615a69b src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Sep 09 16:43:57 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Sep 09 17:23:03 2010 +0200
@@ -96,7 +96,7 @@
 fun invoke_quickcheck quickcheck_generator thy t =
   TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
       (fn _ =>
-          case Quickcheck.gen_test_term (ProofContext.init_global thy) true true (SOME quickcheck_generator)
+          case Quickcheck.gen_test_term (ProofContext.init_global thy) true (SOME quickcheck_generator)
                                     size iterations (preprocess thy [] t) of
             (NONE, (time_report, report)) => (NoCex, (time_report, report))
           | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()