--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Tue Dec 20 18:59:50 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Wed Dec 21 09:21:35 2011 +0100
@@ -46,10 +46,14 @@
in
(descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], []))
end
+ fun ensure_sort (sort, instantiate) =
+ Quickcheck_Common.ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
+ (the_descr, instantiate))
+ Datatype_Aux.default_config [tyco]
in
- Quickcheck_Common.ensure_sort (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}),
- (the_descr, Exhaustive_Generators.instantiate_full_exhaustive_datatype))
- Datatype_Aux.default_config [tyco] thy
+ thy
+ |> ensure_sort (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype)
+ |> ensure_sort (@{sort random}, Random_Generators.instantiate_random_datatype)
end
val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
--- 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;