src/HOL/Tools/Quickcheck/exhaustive_generators.ML
changeset 45924 f03dd48829d8
parent 45923 473b744c23f2
child 46042 ab32a87ba01a
--- 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 =