--- a/src/HOL/Mutabelle/mutabelle.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Fri Dec 03 08:40:47 2010 +0100
@@ -497,9 +497,9 @@
(map_types (inst_type insts) (freeze t));
fun is_executable thy insts th =
- ((Quickcheck.test_term
+ ((Quickcheck.test_term
((Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) (ProofContext.init_global thy))
- (SOME (!testgen_name)) (preprocess thy insts (prop_of th));
+ false (SOME (!testgen_name)) (preprocess thy insts (prop_of th));
Output.urgent_message "executable"; true) handle ERROR s =>
(Output.urgent_message ("not executable: " ^ s); false));
@@ -509,7 +509,7 @@
((x, pretty (the_default [] (fst (Quickcheck.test_term
((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter)
(ProofContext.init_global usedthy))
- (SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc))
+ false (SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc))
handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);