--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Feb 21 11:25:48 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Feb 21 12:20:33 2012 +0100
@@ -23,6 +23,9 @@
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
+ val instantiate_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 =