--- 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);
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Feb 11 11:47:43 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Feb 11 11:47:44 2011 +0100
@@ -122,7 +122,7 @@
TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
(fn _ =>
case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
- false [] [t] of
+ (false, false) [] [t] of
(NONE, _) => (NoCex, ([], NONE))
| (SOME _, _) => (GenuineCex, ([], NONE))) ()
handle TimeLimit.TimeOut =>
@@ -315,7 +315,7 @@
((Config.put Quickcheck.finite_types true #>
Config.put Quickcheck.finite_type_size 1 #>
Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
- false [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
+ (false, false) [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
end
fun is_executable_thm thy th = is_executable_term thy (prop_of th)