src/Provers/classical.ML

--- a/src/Provers/classical.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/classical.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -124,7 +124,6 @@
     (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
   val cla_method':
     (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
-  val setup: theory -> theory
 end;
 
 
@@ -882,17 +881,18 @@
 val elimN = "elim";
 val destN = "dest";
 
-val setup_attrs =
-  Attrib.setup @{binding swapped} (Scan.succeed swapped)
-    "classical swap of introduction rule" #>
-  Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
-    "declaration of Classical destruction rule" #>
-  Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
-    "declaration of Classical elimination rule" #>
-  Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
-    "declaration of Classical introduction rule" #>
-  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
-    "remove declaration of intro/elim/dest rule";
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding swapped} (Scan.succeed swapped)
+      "classical swap of introduction rule" #>
+    Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
+      "declaration of Classical destruction rule" #>
+    Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
+      "declaration of Classical elimination rule" #>
+    Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
+      "declaration of Classical introduction rule" #>
+    Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
+      "remove declaration of intro/elim/dest rule");
 
 
 
@@ -941,46 +941,40 @@
 
 
 
-(** setup_methods **)
+(** method setup **)
 
-val setup_methods =
-  Method.setup @{binding default}
-   (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
-    "apply some intro/elim rule (potentially classical)" #>
-  Method.setup @{binding rule}
-    (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
-    "apply some intro/elim rule (potentially classical)" #>
-  Method.setup @{binding contradiction}
-    (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
-    "proof by contradiction" #>
-  Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
-    "repeatedly apply safe steps" #>
-  Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
-  Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
-  Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
-  Method.setup @{binding deepen}
-    (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
-      >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
-    "classical prover (iterative deepening)" #>
-  Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
-    "classical prover (apply safe rules)" #>
-  Method.setup @{binding safe_step} (cla_method' safe_step_tac)
-    "single classical step (safe rules)" #>
-  Method.setup @{binding inst_step} (cla_method' inst_step_tac)
-    "single classical step (safe rules, allow instantiations)" #>
-  Method.setup @{binding step} (cla_method' step_tac)
-    "single classical step (safe and unsafe rules)" #>
-  Method.setup @{binding slow_step} (cla_method' slow_step_tac)
-    "single classical step (safe and unsafe rules, allow backtracking)" #>
-  Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
-    "single classical step (safe rules, without splitting)";
-
-
-
-(** theory setup **)
-
-val setup = setup_attrs #> setup_methods;
-
+val _ =
+  Theory.setup
+   (Method.setup @{binding default}
+     (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
+      "apply some intro/elim rule (potentially classical)" #>
+    Method.setup @{binding rule}
+      (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
+      "apply some intro/elim rule (potentially classical)" #>
+    Method.setup @{binding contradiction}
+      (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
+      "proof by contradiction" #>
+    Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
+      "repeatedly apply safe steps" #>
+    Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
+    Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
+    Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
+    Method.setup @{binding deepen}
+      (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
+        >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
+      "classical prover (iterative deepening)" #>
+    Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
+      "classical prover (apply safe rules)" #>
+    Method.setup @{binding safe_step} (cla_method' safe_step_tac)
+      "single classical step (safe rules)" #>
+    Method.setup @{binding inst_step} (cla_method' inst_step_tac)
+      "single classical step (safe rules, allow instantiations)" #>
+    Method.setup @{binding step} (cla_method' step_tac)
+      "single classical step (safe and unsafe rules)" #>
+    Method.setup @{binding slow_step} (cla_method' slow_step_tac)
+      "single classical step (safe and unsafe rules, allow backtracking)" #>
+    Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
+      "single classical step (safe rules, without splitting)");
 
 
 (** outer syntax **)