--- a/src/HOL/Tools/smallvalue_generators.ML Wed Mar 09 21:40:38 2011 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML Fri Mar 11 08:12:55 2011 +0100
@@ -375,9 +375,7 @@
Datatype.interpretation
(Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
#> setup_smart_quantifier
- #> Context.theory_map
- (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
- #> Context.theory_map
- (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
+ #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
+ #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
end;