# HG changeset patch
# User wenzelm
# Date 1414590014 -3600
# Node ID 3ad2759acc52152d2003c408d3e3c0c3479c05a3
# Parent  aa43c6f05bcaea46cfab4d6f89597d8d05b04cb4
modernized setup;

diff -r aa43c6f05bca -r 3ad2759acc52 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Nat.thy	Wed Oct 29 14:40:14 2014 +0100
@@ -1599,8 +1599,6 @@
   shows "u = s"
   using 2 1 by (rule trans)
 
-setup Arith_Data.setup
-
 ML_file "Tools/nat_arith.ML"
 
 simproc_setup nateq_cancel_sums
diff -r aa43c6f05bca -r 3ad2759acc52 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Presburger.thy	Wed Oct 29 14:40:14 2014 +0100
@@ -390,7 +390,6 @@
   by (simp cong: conj_cong)
 
 ML_file "Tools/Qelim/cooper.ML"
-setup Cooper.setup
 
 method_setup presburger = {*
   let
diff -r aa43c6f05bca -r 3ad2759acc52 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Product_Type.thy	Wed Oct 29 14:40:14 2014 +0100
@@ -784,7 +784,6 @@
   by (simp only: internal_split_def split_conv)
 
 ML_file "Tools/split_rule.ML"
-setup Split_Rule.setup
 
 hide_const internal_split
 
diff -r aa43c6f05bca -r 3ad2759acc52 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 29 14:40:14 2014 +0100
@@ -13,7 +13,6 @@
   exception COOPER of string
   val conv: Proof.context -> conv
   val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
-  val setup: theory -> theory
 end;
 
 structure Cooper: COOPER =
@@ -835,6 +834,7 @@
       [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
        @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
 in
+
 fun nat_to_int_tac ctxt = 
   simp_tac (put_simpset ss1 ctxt) THEN_ALL_NEW
   simp_tac (put_simpset ss2 ctxt) THEN_ALL_NEW
@@ -842,16 +842,17 @@
 
 fun div_mod_tac ctxt = simp_tac (put_simpset div_mod_ss ctxt);
 fun splits_tac ctxt = simp_tac (put_simpset splits_ss ctxt);
+
 end;
 
 fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
    let
-    val cpth = 
+     val cpth = 
        if Config.get ctxt quick_and_dirty
        then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (term_of (Thm.dest_arg p))))
        else Conv.arg_conv (conv ctxt) p
-    val p' = Thm.rhs_of cpth
-    val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
+     val p' = Thm.rhs_of cpth
+     val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
    in rtac th i end
    handle COOPER _ => no_tac);
 
@@ -881,7 +882,7 @@
   end 1);
 
 
-(* theory setup *)
+(* attribute syntax *)
 
 local
 
@@ -896,11 +897,12 @@
 
 in
 
-val setup =
-  Attrib.setup @{binding presburger}
-    ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
-      optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
-  #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] []));
+val _ =
+  Theory.setup
+    (Attrib.setup @{binding presburger}
+      ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+        optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
+    #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] [])));
 
 end;
 
diff -r aa43c6f05bca -r 3ad2759acc52 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Tools/arith_data.ML	Wed Oct 29 14:40:14 2014 +0100
@@ -20,8 +20,6 @@
   val prove_conv2: tactic -> (Proof.context -> tactic) -> Proof.context -> term * term -> thm
   val simp_all_tac: thm list -> Proof.context -> tactic
   val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
-
-  val setup: theory -> theory
 end;
 
 structure Arith_Data: ARITH_DATA =
@@ -48,14 +46,15 @@
 val arith_tac = gen_arith_tac false;
 val verbose_arith_tac = gen_arith_tac true;
 
-val setup =
-  Method.setup @{binding arith}
-    (Scan.succeed (fn ctxt =>
-      METHOD (fn facts =>
-        HEADGOAL
-        (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
-          THEN' verbose_arith_tac ctxt))))
-    "various arithmetic decision procedures";
+val _ =
+  Theory.setup
+    (Method.setup @{binding arith}
+      (Scan.succeed (fn ctxt =>
+        METHOD (fn facts =>
+          HEADGOAL
+          (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
+            THEN' verbose_arith_tac ctxt))))
+      "various arithmetic decision procedures");
 
 
 (* some specialized syntactic operations *)
diff -r aa43c6f05bca -r 3ad2759acc52 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Tools/split_rule.ML	Wed Oct 29 14:40:14 2014 +0100
@@ -9,7 +9,6 @@
   val split_rule_var: Proof.context -> term -> thm -> thm
   val split_rule: Proof.context -> thm -> thm
   val complete_split_rule: Proof.context -> thm -> thm
-  val setup: theory -> theory
 end;
 
 structure Split_Rule: SPLIT_RULE =
@@ -110,14 +109,15 @@
 
 (* attribute syntax *)
 
-val setup =
-  Attrib.setup @{binding split_format}
-    (Scan.lift (Args.parens (Args.$$$ "complete")
-      >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
-    "split pair-typed subterms in premises, or function arguments" #>
-  Attrib.setup @{binding split_rule}
-    (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
-    "curries ALL function variables occurring in a rule's conclusion";
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding split_format}
+      (Scan.lift (Args.parens (Args.$$$ "complete")
+        >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
+      "split pair-typed subterms in premises, or function arguments" #>
+    Attrib.setup @{binding split_rule}
+      (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
+      "curries ALL function variables occurring in a rule's conclusion");
 
 end;