# HG changeset patch
# User wenzelm
# Date 1414577604 -3600
# Node ID 5a9a2d3b9f8b5b7ddae8c7d2c563911a41087b68
# Parent  19382bbfa93aeeaa189a61d4843fdb9158e570b4
modernized setup;

diff -r 19382bbfa93a -r 5a9a2d3b9f8b src/HOL/Library/Predicate_Compile_Quickcheck.thy
--- 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
diff -r 19382bbfa93a -r 5a9a2d3b9f8b src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- 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