src/HOL/Mutabelle/mutabelle.ML

--- a/src/HOL/Mutabelle/mutabelle.ML	Fri Feb 11 11:47:43 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Fri Feb 11 11:47:44 2011 +0100
@@ -500,7 +500,7 @@
       |> Config.put Quickcheck.size 1
       |> Config.put Quickcheck.iterations 1
       |> Config.put Quickcheck.tester (!testgen_name))
-      false (preprocess thy insts (prop_of th));
+      (true, false) (preprocess thy insts (prop_of th));
     Output.urgent_message "executable"; true) handle ERROR s =>
     (Output.urgent_message ("not executable: " ^ s); false));
 
@@ -511,7 +511,7 @@
        ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter
         #> Config.put Quickcheck.tester (!testgen_name))
          (ProofContext.init_global usedthy))
-       false (preprocess usedthy insts x))))) :: acc))
+       (true, false) (preprocess usedthy insts x))))) :: acc))
           handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);