# HG changeset patch
# User bulwahn
# Date 1299853273 -3600
# Node ID 05abcee548a117ed4af00ea6e1f434b23bdc2c5d
# Parent  8759e9d043f9582f7896a3c3b4a209d503ba186d
adaptions in generators using the common functions

diff -r 8759e9d043f9 -r 05abcee548a1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 11 15:21:13 2011 +0100
@@ -338,6 +338,7 @@
   Tools/Qelim/qelim.ML \
   Tools/Quickcheck/exhaustive_generators.ML \
   Tools/Quickcheck/random_generators.ML \
+  Tools/Quickcheck/quickcheck_common.ML \
   Tools/Quotient/quotient_def.ML \
   Tools/Quotient/quotient_info.ML \
   Tools/Quotient/quotient_tacs.ML \
diff -r 8759e9d043f9 -r 05abcee548a1 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Quickcheck.thy	Fri Mar 11 15:21:13 2011 +0100
@@ -4,7 +4,9 @@
 
 theory Quickcheck
 imports Random Code_Evaluation Enum
-uses ("Tools/Quickcheck/random_generators.ML")
+uses
+  "Tools/Quickcheck/quickcheck_common.ML"
+  ("Tools/Quickcheck/random_generators.ML")
 begin
 
 notation fcomp (infixl "\<circ>>" 60)
diff -r 8759e9d043f9 -r 05abcee548a1 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -396,7 +396,7 @@
 
 val setup =
   Datatype.interpretation
-    (Quickcheck_Generators.ensure_sort_datatype (@{sort exhaustive}, instantiate_exhaustive_datatype))
+    (Quickcheck_Common.ensure_sort_datatype (@{sort exhaustive}, instantiate_exhaustive_datatype))
   #> setup_smart_quantifier
   #> setup_quickcheck_pretty
   #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
diff -r 8759e9d043f9 -r 05abcee548a1 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -427,7 +427,7 @@
 (** setup **)
 
 val setup =
-  Datatype.interpretation (ensure_sort_datatype (@{sort random}, instantiate_random_datatype))
+  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype (@{sort random}, instantiate_random_datatype))
   #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
   #> Context.theory_map
     (Quickcheck.add_generator ("random", compile_generator_expr));
diff -r 8759e9d043f9 -r 05abcee548a1 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/record.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -1835,7 +1835,7 @@
   in
     if has_inst then thy
     else
-      (case Random_Generators.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of
+      (case Quickcheck_Common.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of
         SOME constrain =>
           instantiate_random_record ext_tyco (map constrain vs) extN
             ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy