# HG changeset patch
# User bulwahn
# Date 1324398151 -3600
# Node ID f03dd48829d8467e8dd8e76348b0c13ca14d22c5
# Parent  473b744c23f2569ce39257e3a9bca8b464a380ee
exporting instantiation functions in quickcheck for their usage in abstract generators

diff -r 473b744c23f2 -r f03dd48829d8 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Dec 20 17:22:31 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Dec 20 17:22:31 2011 +0100
@@ -20,6 +20,9 @@
   val quickcheck_pretty : bool Config.T
   val setup_exhaustive_datatype_interpretation : theory -> theory
   val setup: theory -> theory
+  
+  val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
+    (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
 end;
 
 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =