# HG changeset patch
# User bulwahn
# Date 1321265646 -3600
# Node ID 23871e17dddb584a04141583563705127a7ccf00
# Parent  8f32682f78fee1fcfe1bef6199e2235d4d250312
setting up exhaustive generators which are used for the smart generators

diff -r 8f32682f78fe -r 23871e17dddb src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- 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))))
diff -r 8f32682f78fe -r 23871e17dddb src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- 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 =