--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sun Jul 17 22:25:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 18 10:34:21 2011 +0200
@@ -438,14 +438,15 @@
end
end;
-
+val test_goals = Quickcheck.generator_test_goal_terms;
+
(** setup **)
val setup =
Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort typerep}, @{sort term_of}), @{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));
+ #> Context.theory_map (Quickcheck.add_generator ("random", compile_generator_expr))
+ #> Context.theory_map (Quickcheck.add_tester ("random", test_goals));
end;