# HG changeset patch
# User bulwahn
# Date 1324455695 -3600
# Node ID 71970a26a2696005dc80ce9c24c9f59f2b0f856b
# Parent  711fec5b4f6116337d0496d9bedcba0698f5a968
quickcheck_generator command also creates random generators

diff -r 711fec5b4f61 -r 71970a26a269 src/HOL/Tools/Quickcheck/abstract_generators.ML
--- 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)
diff -r 711fec5b4f61 -r 71970a26a269 src/HOL/Tools/Quickcheck/random_generators.ML
--- 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;