# HG changeset patch
# User bulwahn
# Date 1321270159 -3600
# Node ID 7a0975c9dd2666712b8467650db4fb6bb2b71370
# Parent  23871e17dddb584a04141583563705127a7ccf00# Parent  34d07cf7d2074cf5734128824527778af7833768
merged

diff -r 34d07cf7d207 -r 7a0975c9dd26 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Nov 14 11:50:52 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Nov 14 12:29:19 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 34d07cf7d207 -r 7a0975c9dd26 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Nov 14 11:50:52 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Nov 14 12:29:19 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 =