# HG changeset patch
# User bulwahn
# Date 1341222319 -7200
# Node ID 0192811f0a961ece1b2ef8cbc05764716d33b88b
# Parent  eb72f99737be80d7f94a5f28034fba7541539222
exporting important function for the "many conjecture refutation" compilation of quickcheck

diff -r eb72f99737be -r 0192811f0a96 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 02 11:39:24 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 02 11:45:19 2012 +0200
@@ -20,6 +20,7 @@
   val optimise_equality : bool Config.T
   val quickcheck_pretty : bool Config.T
   val setup_exhaustive_datatype_interpretation : theory -> theory
+  val setup_bounded_forall_datatype_interpretation : theory -> theory
   val setup: theory -> theory
   
   val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
@@ -564,6 +565,11 @@
 val setup_exhaustive_datatype_interpretation =
   Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype)
 
+val setup_bounded_forall_datatype_interpretation =
+  Datatype.interpretation (Quickcheck_Common.ensure_sort
+    (((@{sort type}, @{sort type}), @{sort bounded_forall}),
+    (Datatype.the_descr, instantiate_bounded_forall_datatype)))
+
 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
 
 val setup =