src/HOL/Tools/Quickcheck/random_generators.ML
changeset 45940 71970a26a269
parent 45923 473b744c23f2
child 46331 f5598b604a54
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Dec 20 18:59:50 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Dec 21 09:21:35 2011 +0100
@@ -16,6 +16,8 @@
     -> Proof.context -> Proof.context
   val put_counterexample_report: (unit -> int -> bool -> int -> seed -> ((bool * term list) option * (bool list * bool)) * seed)
     -> Proof.context -> Proof.context
+  val instantiate_random_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
+    (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
   val setup: theory -> theory
 end;