--- 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))))