--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Sep 05 00:41:01 2014 +0200
@@ -7,6 +7,7 @@
signature RANDOM_GENERATORS =
sig
type seed = Random_Engine.seed
+ val random_interpretation: string
val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-> seed -> (('a -> 'b) * (unit -> term)) * seed
@@ -24,6 +25,8 @@
structure Random_Generators : RANDOM_GENERATORS =
struct
+val random_interpretation = "random";
+
(** abstract syntax **)
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
@@ -471,7 +474,8 @@
val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
val setup =
- Quickcheck_Common.datatype_interpretation (@{sort random}, instantiate_random_datatype)
+ Quickcheck_Common.datatype_interpretation random_interpretation
+ (@{sort random}, instantiate_random_datatype)
#> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
end;