--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 18 10:34:21 2011 +0200
@@ -501,7 +501,6 @@
(((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
- #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
#> Context.theory_map (Quickcheck.add_tester ("exhaustive", test_goals))
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
#> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));