--- 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 \
--- 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)
--- 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))
--- 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));
--- 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