--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy Wed Oct 29 10:58:41 2014 +0100
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy Wed Oct 29 11:13:24 2014 +0100
@@ -8,6 +8,4 @@
ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
-setup {* Predicate_Compile_Quickcheck.setup *}
-
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Oct 29 10:58:41 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Oct 29 11:13:24 2014 +0100
@@ -31,7 +31,6 @@
val nrandom : int Unsynchronized.ref
val debug : bool Unsynchronized.ref
val no_higher_order_predicate : string list Unsynchronized.ref
- val setup : theory -> theory
end;
structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
@@ -423,11 +422,12 @@
val smart_slow_exhaustive_active =
Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false)
-val setup =
- Exhaustive_Generators.setup_exhaustive_datatype_interpretation
- #> Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
- (smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false))))
- #> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
- (smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false))))
+val _ =
+ Theory.setup
+ (Exhaustive_Generators.setup_exhaustive_datatype_interpretation #>
+ Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
+ (smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false)))) #>
+ Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
+ (smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false)))))
end