--- a/src/HOL/Tools/Quickcheck/random_generators.ML Tue Dec 20 14:43:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Tue Dec 20 17:22:31 2011 +0100
@@ -460,8 +460,7 @@
val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
val setup =
- Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
- (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
+ Quickcheck_Common.datatype_interpretation (@{sort random}, instantiate_random_datatype)
#> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
end;