# HG changeset patch
# User wenzelm
# Date 1334248759 -7200
# Node ID e1576d13e9339e2b33341684f04d88538be4e4be
# Parent  d9dd4a9f18fc61101b64a624e4650bcb931bb915
more standard method setup;

diff -r d9dd4a9f18fc -r e1576d13e933 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/CCL/Wfd.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -493,26 +493,19 @@
 subsection {* Evaluation *}
 
 ML {*
-
-local
-  structure Data = Named_Thms(val name = @{binding eval} val description = "evaluation rules");
-in
+structure Eval_Rules =
+  Named_Thms(val name = @{binding eval} val description = "evaluation rules");
 
 fun eval_tac ths =
   Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
-    DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
+    DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Eval_Rules.get context) 1));
+*}
+setup Eval_Rules.setup
 
-val eval_setup =
-  Data.setup #>
-  Method.setup @{binding eval}
-    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt)))
-    "evaluation";
-
-end;
-
+method_setup eval = {*
+  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))
 *}
 
-setup eval_setup
 
 lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam
 
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Auth/Smartcard/ShoupRubin.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -762,7 +762,7 @@
 
 method_setup prepare = {*
     Scan.succeed (K (SIMPLE_METHOD ShoupRubin.prepare_tac)) *}
-  "to launch a few simple facts that'll help the simplifier"
+  "to launch a few simple facts that will help the simplifier"
 
 method_setup parts_prepare = {*
     Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Auth/Smartcard/ShoupRubinBella.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -771,7 +771,7 @@
 
 method_setup prepare = {*
     Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
-  "to launch a few simple facts that'll help the simplifier"
+  "to launch a few simple facts that will help the simplifier"
 
 method_setup parts_prepare = {*
     Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Boogie/Tools/boogie_tactics.ML
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -45,12 +45,12 @@
     in tac ctxt (thms @ facts) end))
 
 val setup_boogie = Method.setup @{binding boogie} (boogie_method false)
-  ("Applies an SMT solver to the current goal " ^
-   "using the current set of Boogie background axioms")
+  "apply an SMT solver to the current goal \
+  \using the current set of Boogie background axioms"
 
 val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true)
-  ("Applies an SMT solver to all goals " ^
-   "using the current set of Boogie background axioms")
+  "apply an SMT solver to all goals \
+  \using the current set of Boogie background axioms"
 
 
 local
@@ -96,7 +96,7 @@
 in
 val setup_boogie_cases = Method.setup @{binding boogie_cases}
   (Scan.succeed boogie_cases)
-  "Prepares a set of Boogie assertions for case-based proofs"
+  "prepare a set of Boogie assertions for case-based proofs"
 end
 
 
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -314,6 +314,9 @@
 
 
 use "commutative_ring_tac.ML"
-setup Commutative_Ring_Tac.setup
+
+method_setup comm_ring = {*
+  Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
+*} "reflective decision procedure for equalities over commutative rings"
 
 end
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -2005,7 +2005,12 @@
 *}
 
 use "cooper_tac.ML"
-setup "Cooper_Tac.setup"
+
+method_setup cooper = {*
+  Args.mode "no_quantify" >>
+    (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q)))
+*} "decision procedure for linear integer arithmetic"
+
 
 text {* Tests *}
 
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -2004,7 +2004,12 @@
 *}
 
 use "ferrack_tac.ML"
-setup Ferrack_Tac.setup
+
+method_setup rferrack = {*
+  Args.mode "no_quantify" >>
+    (fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q)))
+*} "decision procedure for linear real arithmetic"
+
 
 lemma
   fixes x :: real
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -5635,7 +5635,12 @@
 *}
 
 use "mir_tac.ML"
-setup "Mir_Tac.setup"
+
+method_setup mir = {*
+  Args.mode "no_quantify" >>
+    (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
+*} "decision procedure for MIR arithmetic"
+
 
 lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
   by mir
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Decision_Procs/commutative_ring_tac.ML
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -7,7 +7,6 @@
 signature COMMUTATIVE_RING_TAC =
 sig
   val tac: Proof.context -> int -> tactic
-  val setup: theory -> theory
 end
 
 structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC =
@@ -98,8 +97,4 @@
     THEN (simp_tac cring_ss i)
   end);
 
-val setup =
-  Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o tac))
-    "reflective decision procedure for equalities over commutative rings";
-
 end;
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -6,7 +6,6 @@
 sig
   val trace: bool Unsynchronized.ref
   val linz_tac: Proof.context -> bool -> int -> tactic
-  val setup: theory -> theory
 end
 
 structure Cooper_Tac: COOPER_TAC =
@@ -115,15 +114,4 @@
       | _ => (pre_thm, assm_tac i)
   in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
 
-val setup =
-  Method.setup @{binding cooper}
-    let
-      val parse_flag = Args.$$$ "no_quantify" >> K (K false)
-    in
-      Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
-        curry (Library.foldl op |>) true) >>
-      (fn q => fn ctxt => SIMPLE_METHOD' (linz_tac ctxt q))
-    end
-    "decision procedure for linear integer arithmetic";
-
 end
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -6,7 +6,6 @@
 sig
   val trace: bool Unsynchronized.ref
   val linr_tac: Proof.context -> bool -> int -> tactic
-  val setup: theory -> theory
 end
 
 structure Ferrack_Tac =
@@ -96,10 +95,4 @@
       | _ => (pre_thm, assm_tac i)
   in rtac ((mp_step nh o spec_step np) th) i THEN tac end);
 
-val setup =
-  Method.setup @{binding rferrack}
-    (Args.mode "no_quantify" >> (fn q => fn ctxt =>
-      SIMPLE_METHOD' (linr_tac ctxt (not q))))
-    "decision procedure for linear real arithmetic";
-
 end
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -6,7 +6,6 @@
 sig
   val trace: bool Unsynchronized.ref
   val mir_tac: Proof.context -> bool -> int -> tactic
-  val setup: theory -> theory
 end
 
 structure Mir_Tac =
@@ -143,15 +142,4 @@
       | _ => (pre_thm, assm_tac i)
   in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
 
-val setup =
-  Method.setup @{binding mir}
-    let
-      val parse_flag = Args.$$$ "no_quantify" >> K (K false)
-    in
-      Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
-        curry (Library.foldl op |>) true) >>
-      (fn q => fn ctxt => SIMPLE_METHOD' (mir_tac ctxt q))
-    end
-    "decision procedure for MIR arithmetic";
-
 end
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/FunDef.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -110,14 +110,21 @@
 use "Tools/Function/relation.ML"
 use "Tools/Function/function.ML"
 use "Tools/Function/pat_completeness.ML"
+
+method_setup pat_completeness = {*
+  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
+*} "prove completeness of datatype patterns"
+
 use "Tools/Function/fun.ML"
 use "Tools/Function/induction_schema.ML"
 
+method_setup induction_schema = {*
+  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
+*} "prove an induction principle"
+
 setup {* 
   Function.setup
-  #> Pat_Completeness.setup
   #> Function_Fun.setup
-  #> Induction_Schema.setup
 *}
 
 subsection {* Measure Functions *}
@@ -137,6 +144,12 @@
 by (rule is_measure_trivial)
 
 use "Tools/Function/lexicographic_order.ML"
+
+method_setup lexicographic_order = {*
+  Method.sections clasimp_modifiers >>
+  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
+*} "termination prover for lexicographic orderings"
+
 setup Lexicographic_Order.setup 
 
 
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Groebner_Basis.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -43,8 +43,20 @@
 
 use "Tools/groebner.ML"
 
-method_setup algebra = Groebner.algebra_method
-  "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
+method_setup algebra = {*
+  let
+    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+    val addN = "add"
+    val delN = "del"
+    val any_keyword = keyword addN || keyword delN
+    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+  in
+    Scan.optional (keyword addN |-- thms) [] --
+     Scan.optional (keyword delN |-- thms) [] >>
+    (fn (add_ths, del_ths) => fn ctxt =>
+      SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
+  end
+*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
 
 declare dvd_def[algebra]
 declare dvd_eq_mod_eq_0[symmetric, algebra]
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/HOLCF/Fixrec.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -230,7 +230,9 @@
 use "Tools/holcf_library.ML"
 use "Tools/fixrec.ML"
 
-setup {* Fixrec.setup *}
+method_setup fixrec_simp = {*
+  Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
+*} "pattern prover for fixrec constants"
 
 setup {*
   Fixrec.add_matchers
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -12,7 +12,6 @@
     -> (bool * (Attrib.binding * string)) list -> local_theory -> local_theory
   val add_matchers: (string * string) list -> theory -> theory
   val fixrec_simp_tac: Proof.context -> int -> tactic
-  val setup: theory -> theory
 end
 
 structure Fixrec : FIXREC =
@@ -406,9 +405,4 @@
     (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
       >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
 
-val setup =
-  Method.setup @{binding fixrec_simp}
-    (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))
-    "pattern prover for fixrec constants"
-
 end
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Library/Countable.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -269,8 +269,7 @@
     by - (rule exI)
 qed
 
-method_setup countable_datatype = {*
-let
+ML {*
   fun countable_tac ctxt =
     SUBGOAL (fn (goal, i) =>
       let
@@ -297,9 +296,10 @@
            etac induct_thm i,
            REPEAT (resolve_tac rules i ORELSE atac i)]) 1
       end)
-in
+*}
+
+method_setup countable_datatype = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt))
-end
 *} "prove countable class instances for datatypes"
 
 hide_const (open) finite_item nth_item
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -77,8 +77,8 @@
 
 method_setup eval_witness = {*
   Scan.lift (Scan.repeat Args.name) >>
-  (fn ws => K (SIMPLE_METHOD'
-    (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
+    (fn ws => K (SIMPLE_METHOD'
+      (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
 *} "evaluation with ML witnesses"
 
 
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Limits.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -112,7 +112,8 @@
 qed
 
 ML {*
-  fun ev_elim_tac ctxt thms thm = let
+  fun eventually_elim_tac ctxt thms thm =
+    let
       val thy = Proof_Context.theory_of ctxt
       val mp_thms = thms RL [@{thm eventually_rev_mp}]
       val raw_elim_thm =
@@ -124,13 +125,11 @@
     in
       CASES cases (rtac raw_elim_thm 1) thm
     end
-
-  fun eventually_elim_setup name =
-    Method.setup name (Scan.succeed (fn ctxt => METHOD_CASES (ev_elim_tac ctxt)))
-      "elimination of eventually quantifiers"
 *}
 
-setup {* eventually_elim_setup @{binding "eventually_elim"} *}
+method_setup eventually_elim = {*
+  Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
+*} "elimination of eventually quantifiers"
 
 
 subsection {* Finer-than relation *}
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -91,6 +91,12 @@
 use "transfer.ML"
 setup Transfer_Principle.setup
 
+method_setup transfer = {*
+  Attrib.thms >> (fn ths => fn ctxt =>
+    SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))
+*} "transfer principle"
+
+
 text {* Transfer introduction rules. *}
 
 lemma transfer_ex [transfer_intro]:
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/NSA/transfer.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -112,8 +112,6 @@
   Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
     "declaration of transfer unfolding rule" #>
   Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
-    "declaration of transfer refolding rule" #>
-  Method.setup @{binding transfer} (Attrib.thms >> (fn ths => fn ctxt =>
-    SIMPLE_METHOD' (transfer_tac ctxt ths))) "transfer principle";
+    "declaration of transfer refolding rule"
 
 end;
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Orderings.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -312,7 +312,7 @@
 signature ORDERS =
 sig
   val print_structures: Proof.context -> unit
-  val setup: theory -> theory
+  val attrib_setup: theory -> theory
   val order_tac: Proof.context -> thm list -> int -> tactic
 end;
 
@@ -414,19 +414,15 @@
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
         Toplevel.keep (print_structures o Toplevel.context_of)));
 
-
-(** Setup **)
-
-val setup =
-  Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt [])))
-    "transitivity reasoner" #>
-  attrib_setup;
-
 end;
 
 *}
 
-setup Orders.setup
+setup Orders.attrib_setup
+
+method_setup order = {*
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
+*} "transitivity reasoner"
 
 
 text {* Declarations to set up transitivity reasoner of partial and linear orders. *}
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Presburger.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -387,10 +387,25 @@
   by (simp cong: conj_cong)
 
 use "Tools/Qelim/cooper.ML"
-
 setup Cooper.setup
 
-method_setup presburger = "Cooper.method" "Cooper's algorithm for Presburger arithmetic"
+method_setup presburger = {*
+  let
+    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+    fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
+    val addN = "add"
+    val delN = "del"
+    val elimN = "elim"
+    val any_keyword = keyword addN || keyword delN || simple_keyword elimN
+    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+  in
+    Scan.optional (simple_keyword elimN >> K false) true --
+    Scan.optional (keyword addN |-- thms) [] --
+    Scan.optional (keyword delN |-- thms) [] >>
+    (fn ((elim, add_ths), del_ths) => fn ctxt =>
+      SIMPLE_METHOD' (Cooper.tac elim add_ths del_ths ctxt))
+  end
+*} "Cooper's algorithm for Presburger arithmetic"
 
 declare dvd_eq_mod_eq_0[symmetric, presburger]
 declare mod_1[presburger] 
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -9,7 +9,6 @@
   val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
                    -> Proof.context -> thm list -> tactic
   val induction_schema_tac : Proof.context -> thm list -> tactic
-  val setup : theory -> theory
 end
 
 
@@ -395,8 +394,4 @@
 fun induction_schema_tac ctxt =
   mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
 
-val setup =
-  Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac))
-    "proves an induction principle"
-
 end
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -9,8 +9,6 @@
 sig
   val lex_order_tac : bool -> Proof.context -> tactic -> tactic
   val lexicographic_order_tac : bool -> Proof.context -> tactic
-  val lexicographic_order : Proof.context -> Proof.method
-
   val setup: theory -> theory
 end
 
@@ -218,12 +216,7 @@
   lex_order_tac quiet ctxt
     (auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
 
-val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
-
 val setup =
-  Method.setup @{binding lexicographic_order}
-    (Method.sections clasimp_modifiers >> (K lexicographic_order))
-    "termination prover for lexicographic orderings"
-  #> Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
+  Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
 
 end;
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Tools/Function/pat_completeness.ML
--- a/src/HOL/Tools/Function/pat_completeness.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -7,11 +7,8 @@
 signature PAT_COMPLETENESS =
 sig
     val pat_completeness_tac: Proof.context -> int -> tactic
-    val pat_completeness: Proof.context -> Proof.method
     val prove_completeness : theory -> term list -> term -> term list list ->
       term list list -> thm
-
-    val setup : theory -> theory
 end
 
 structure Pat_Completeness : PAT_COMPLETENESS =
@@ -153,11 +150,4 @@
   end
   handle COMPLETENESS => no_tac)
 
-
-val pat_completeness = SIMPLE_METHOD' o pat_completeness_tac
-
-val setup =
-  Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
-    "Completeness prover for datatype patterns"
-
 end
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -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 method: (Proof.context -> Method.method) context_parser
   val setup: theory -> theory
 end;
 
@@ -857,23 +856,6 @@
   THEN_ALL_NEW finish_tac elim
 end;
 
-val method =
-  let
-    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
-    fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
-    val addN = "add"
-    val delN = "del"
-    val elimN = "elim"
-    val any_keyword = keyword addN || keyword delN || simple_keyword elimN
-    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-  in
-    Scan.optional (simple_keyword elimN >> K false) true --
-    Scan.optional (keyword addN |-- thms) [] --
-    Scan.optional (keyword delN |-- thms) [] >>
-    (fn ((elim, add_ths), del_ths) => fn ctxt =>
-      SIMPLE_METHOD' (tac elim add_ths del_ths ctxt))
-  end;
-
 
 (* theory setup *)
 
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/groebner.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -16,7 +16,6 @@
   val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
   val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
   val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
-  val algebra_method: (Proof.context -> Method.method) context_parser
 end
 
 structure Groebner : GROEBNER =
@@ -1027,21 +1026,4 @@
 fun algebra_tac add_ths del_ths ctxt i =
  ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
 
-local
-
-fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
-val addN = "add"
-val delN = "del"
-val any_keyword = keyword addN || keyword delN
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-
-in
-
-val algebra_method = ((Scan.optional (keyword addN |-- thms) []) --
-   (Scan.optional (keyword delN |-- thms) [])) >>
-  (fn (add_ths, del_ths) => fn ctxt =>
-       SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt))
-
 end;
-
-end;
diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -80,11 +80,9 @@
 ML {* sat.trace_sat := false; *}
 ML {* quick_and_dirty := false; *}
 
-method_setup rawsat =
-  {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}
-  "SAT solver (no preprocessing)"
-
-(* ML {* Toplevel.profiling := 1; *} *)
+method_setup rawsat = {*
+  Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
+*} "SAT solver (no preprocessing)"
 
 (* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
 
@@ -512,8 +510,6 @@
    (as of 2006-08-30, on a 2.5 GHz Pentium 4)
 *)
 
-(* ML {* Toplevel.profiling := 0; *} *)
-
 text {*
 Function {\tt benchmark} takes the name of an existing DIMACS CNF
 file, parses this file, passes the problem to a SAT solver, and checks