src/HOL/Tools/Quickcheck/exhaustive_generators.ML

     -> Proof.context -> Proof.context
   val put_validator_batch: (unit -> (int -> bool) list) -> Proof.context -> Proof.context
   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;
 
 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
 struct

 
 val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr);
   
 (* 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 =
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))