--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Nov 14 09:25:05 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Nov 14 11:14:06 2011 +0100
@@ -414,8 +414,9 @@
val smart_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true);
val smart_slow_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false);
-val setup =
- Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
+val setup =
+ Exhaustive_Generators.setup_exhaustive_datatype_interpretation
+ #> Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
(smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false))))
#> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
(smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false))))
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Nov 14 09:25:05 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Nov 14 11:14:06 2011 +0100
@@ -18,6 +18,7 @@
exception Counterexample of term list
val smart_quantifier : bool Config.T
val quickcheck_pretty : bool Config.T
+ val setup_exhaustive_datatype_interpretation : theory -> theory
val setup: theory -> theory
end;
@@ -492,6 +493,10 @@
(* setup *)
+val setup_exhaustive_datatype_interpretation =
+ Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
+
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
val setup =