1.1 --- a/src/CCL/Wfd.thy	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -493,26 +493,19 @@
     1.4  subsection {* Evaluation *}
     1.5  
     1.6  ML {*
     1.7 -
     1.8 -local
     1.9 -  structure Data = Named_Thms(val name = @{binding eval} val description = "evaluation rules");
    1.10 -in
    1.11 +structure Eval_Rules =
    1.12 +  Named_Thms(val name = @{binding eval} val description = "evaluation rules");
    1.13  
    1.14  fun eval_tac ths =
    1.15    Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
    1.16 -    DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
    1.17 +    DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Eval_Rules.get context) 1));
    1.18 +*}
    1.19 +setup Eval_Rules.setup
    1.20  
    1.21 -val eval_setup =
    1.22 -  Data.setup #>
    1.23 -  Method.setup @{binding eval}
    1.24 -    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt)))
    1.25 -    "evaluation";
    1.26 -
    1.27 -end;
    1.28 -
    1.29 +method_setup eval = {*
    1.30 +  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))
    1.31  *}
    1.32  
    1.33 -setup eval_setup
    1.34  
    1.35  lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam
    1.36  

     2.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Thu Apr 12 11:34:50 2012 +0200
     2.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Thu Apr 12 18:39:19 2012 +0200
     2.3 @@ -762,7 +762,7 @@
     2.4  
     2.5  method_setup prepare = {*
     2.6      Scan.succeed (K (SIMPLE_METHOD ShoupRubin.prepare_tac)) *}
     2.7 -  "to launch a few simple facts that'll help the simplifier"
     2.8 +  "to launch a few simple facts that will help the simplifier"
     2.9  
    2.10  method_setup parts_prepare = {*
    2.11      Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}

     3.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Thu Apr 12 11:34:50 2012 +0200
     3.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Thu Apr 12 18:39:19 2012 +0200
     3.3 @@ -771,7 +771,7 @@
     3.4  
     3.5  method_setup prepare = {*
     3.6      Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
     3.7 -  "to launch a few simple facts that'll help the simplifier"
     3.8 +  "to launch a few simple facts that will help the simplifier"
     3.9  
    3.10  method_setup parts_prepare = {*
    3.11      Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}

     4.1 --- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Apr 12 11:34:50 2012 +0200
     4.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Apr 12 18:39:19 2012 +0200
     4.3 @@ -45,12 +45,12 @@
     4.4      in tac ctxt (thms @ facts) end))
     4.5  
     4.6  val setup_boogie = Method.setup @{binding boogie} (boogie_method false)
     4.7 -  ("Applies an SMT solver to the current goal " ^
     4.8 -   "using the current set of Boogie background axioms")
     4.9 +  "apply an SMT solver to the current goal \
    4.10 +  \using the current set of Boogie background axioms"
    4.11  
    4.12  val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true)
    4.13 -  ("Applies an SMT solver to all goals " ^
    4.14 -   "using the current set of Boogie background axioms")
    4.15 +  "apply an SMT solver to all goals \
    4.16 +  \using the current set of Boogie background axioms"
    4.17  
    4.18  
    4.19  local
    4.20 @@ -96,7 +96,7 @@
    4.21  in
    4.22  val setup_boogie_cases = Method.setup @{binding boogie_cases}
    4.23    (Scan.succeed boogie_cases)
    4.24 -  "Prepares a set of Boogie assertions for case-based proofs"
    4.25 +  "prepare a set of Boogie assertions for case-based proofs"
    4.26  end
    4.27  
    4.28  

     5.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Apr 12 11:34:50 2012 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Apr 12 18:39:19 2012 +0200
     5.3 @@ -314,6 +314,9 @@
     5.4  
     5.5  
     5.6  use "commutative_ring_tac.ML"
     5.7 -setup Commutative_Ring_Tac.setup
     5.8 +
     5.9 +method_setup comm_ring = {*
    5.10 +  Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
    5.11 +*} "reflective decision procedure for equalities over commutative rings"
    5.12  
    5.13  end

     6.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Apr 12 11:34:50 2012 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Apr 12 18:39:19 2012 +0200
     6.3 @@ -2005,7 +2005,12 @@
     6.4  *}
     6.5  
     6.6  use "cooper_tac.ML"
     6.7 -setup "Cooper_Tac.setup"
     6.8 +
     6.9 +method_setup cooper = {*
    6.10 +  Args.mode "no_quantify" >>
    6.11 +    (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q)))
    6.12 +*} "decision procedure for linear integer arithmetic"
    6.13 +
    6.14  
    6.15  text {* Tests *}
    6.16  

     7.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Apr 12 11:34:50 2012 +0200
     7.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Apr 12 18:39:19 2012 +0200
     7.3 @@ -2004,7 +2004,12 @@
     7.4  *}
     7.5  
     7.6  use "ferrack_tac.ML"
     7.7 -setup Ferrack_Tac.setup
     7.8 +
     7.9 +method_setup rferrack = {*
    7.10 +  Args.mode "no_quantify" >>
    7.11 +    (fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q)))
    7.12 +*} "decision procedure for linear real arithmetic"
    7.13 +
    7.14  
    7.15  lemma
    7.16    fixes x :: real

     8.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Apr 12 11:34:50 2012 +0200
     8.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Apr 12 18:39:19 2012 +0200
     8.3 @@ -5635,7 +5635,12 @@
     8.4  *}
     8.5  
     8.6  use "mir_tac.ML"
     8.7 -setup "Mir_Tac.setup"
     8.8 +
     8.9 +method_setup mir = {*
    8.10 +  Args.mode "no_quantify" >>
    8.11 +    (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
    8.12 +*} "decision procedure for MIR arithmetic"
    8.13 +
    8.14  
    8.15  lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
    8.16    by mir

     9.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Apr 12 11:34:50 2012 +0200
     9.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Apr 12 18:39:19 2012 +0200
     9.3 @@ -7,7 +7,6 @@
     9.4  signature COMMUTATIVE_RING_TAC =
     9.5  sig
     9.6    val tac: Proof.context -> int -> tactic
     9.7 -  val setup: theory -> theory
     9.8  end
     9.9  
    9.10  structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC =
    9.11 @@ -98,8 +97,4 @@
    9.12      THEN (simp_tac cring_ss i)
    9.13    end);
    9.14  
    9.15 -val setup =
    9.16 -  Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o tac))
    9.17 -    "reflective decision procedure for equalities over commutative rings";
    9.18 -
    9.19  end;

    10.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Apr 12 11:34:50 2012 +0200
    10.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Thu Apr 12 18:39:19 2012 +0200
    10.3 @@ -6,7 +6,6 @@
    10.4  sig
    10.5    val trace: bool Unsynchronized.ref
    10.6    val linz_tac: Proof.context -> bool -> int -> tactic
    10.7 -  val setup: theory -> theory
    10.8  end
    10.9  
   10.10  structure Cooper_Tac: COOPER_TAC =
   10.11 @@ -115,15 +114,4 @@
   10.12        | _ => (pre_thm, assm_tac i)
   10.13    in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
   10.14  
   10.15 -val setup =
   10.16 -  Method.setup @{binding cooper}
   10.17 -    let
   10.18 -      val parse_flag = Args.$$$ "no_quantify" >> K (K false)
   10.19 -    in
   10.20 -      Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
   10.21 -        curry (Library.foldl op |>) true) >>
   10.22 -      (fn q => fn ctxt => SIMPLE_METHOD' (linz_tac ctxt q))
   10.23 -    end
   10.24 -    "decision procedure for linear integer arithmetic";
   10.25 -
   10.26  end

    11.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Apr 12 11:34:50 2012 +0200
    11.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Thu Apr 12 18:39:19 2012 +0200
    11.3 @@ -6,7 +6,6 @@
    11.4  sig
    11.5    val trace: bool Unsynchronized.ref
    11.6    val linr_tac: Proof.context -> bool -> int -> tactic
    11.7 -  val setup: theory -> theory
    11.8  end
    11.9  
   11.10  structure Ferrack_Tac =
   11.11 @@ -96,10 +95,4 @@
   11.12        | _ => (pre_thm, assm_tac i)
   11.13    in rtac ((mp_step nh o spec_step np) th) i THEN tac end);
   11.14  
   11.15 -val setup =
   11.16 -  Method.setup @{binding rferrack}
   11.17 -    (Args.mode "no_quantify" >> (fn q => fn ctxt =>
   11.18 -      SIMPLE_METHOD' (linr_tac ctxt (not q))))
   11.19 -    "decision procedure for linear real arithmetic";
   11.20 -
   11.21  end

    12.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Apr 12 11:34:50 2012 +0200
    12.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Thu Apr 12 18:39:19 2012 +0200
    12.3 @@ -6,7 +6,6 @@
    12.4  sig
    12.5    val trace: bool Unsynchronized.ref
    12.6    val mir_tac: Proof.context -> bool -> int -> tactic
    12.7 -  val setup: theory -> theory
    12.8  end
    12.9  
   12.10  structure Mir_Tac =
   12.11 @@ -143,15 +142,4 @@
   12.12        | _ => (pre_thm, assm_tac i)
   12.13    in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
   12.14  
   12.15 -val setup =
   12.16 -  Method.setup @{binding mir}
   12.17 -    let
   12.18 -      val parse_flag = Args.$$$ "no_quantify" >> K (K false)
   12.19 -    in
   12.20 -      Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
   12.21 -        curry (Library.foldl op |>) true) >>
   12.22 -      (fn q => fn ctxt => SIMPLE_METHOD' (mir_tac ctxt q))
   12.23 -    end
   12.24 -    "decision procedure for MIR arithmetic";
   12.25 -
   12.26  end

    13.1 --- a/src/HOL/FunDef.thy	Thu Apr 12 11:34:50 2012 +0200
    13.2 +++ b/src/HOL/FunDef.thy	Thu Apr 12 18:39:19 2012 +0200
    13.3 @@ -110,14 +110,21 @@
    13.4  use "Tools/Function/relation.ML"
    13.5  use "Tools/Function/function.ML"
    13.6  use "Tools/Function/pat_completeness.ML"
    13.7 +
    13.8 +method_setup pat_completeness = {*
    13.9 +  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
   13.10 +*} "prove completeness of datatype patterns"
   13.11 +
   13.12  use "Tools/Function/fun.ML"
   13.13  use "Tools/Function/induction_schema.ML"
   13.14  
   13.15 +method_setup induction_schema = {*
   13.16 +  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
   13.17 +*} "prove an induction principle"
   13.18 +
   13.19  setup {* 
   13.20    Function.setup
   13.21 -  #> Pat_Completeness.setup
   13.22    #> Function_Fun.setup
   13.23 -  #> Induction_Schema.setup
   13.24  *}
   13.25  
   13.26  subsection {* Measure Functions *}
   13.27 @@ -137,6 +144,12 @@
   13.28  by (rule is_measure_trivial)
   13.29  
   13.30  use "Tools/Function/lexicographic_order.ML"
   13.31 +
   13.32 +method_setup lexicographic_order = {*
   13.33 +  Method.sections clasimp_modifiers >>
   13.34 +  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
   13.35 +*} "termination prover for lexicographic orderings"
   13.36 +
   13.37  setup Lexicographic_Order.setup 
   13.38  
   13.39  

    14.1 --- a/src/HOL/Groebner_Basis.thy	Thu Apr 12 11:34:50 2012 +0200
    14.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Apr 12 18:39:19 2012 +0200
    14.3 @@ -43,8 +43,20 @@
    14.4  
    14.5  use "Tools/groebner.ML"
    14.6  
    14.7 -method_setup algebra = Groebner.algebra_method
    14.8 -  "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    14.9 +method_setup algebra = {*
   14.10 +  let
   14.11 +    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   14.12 +    val addN = "add"
   14.13 +    val delN = "del"
   14.14 +    val any_keyword = keyword addN || keyword delN
   14.15 +    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   14.16 +  in
   14.17 +    Scan.optional (keyword addN |-- thms) [] --
   14.18 +     Scan.optional (keyword delN |-- thms) [] >>
   14.19 +    (fn (add_ths, del_ths) => fn ctxt =>
   14.20 +      SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
   14.21 +  end
   14.22 +*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
   14.23  
   14.24  declare dvd_def[algebra]
   14.25  declare dvd_eq_mod_eq_0[symmetric, algebra]

    15.1 --- a/src/HOL/HOLCF/Fixrec.thy	Thu Apr 12 11:34:50 2012 +0200
    15.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Thu Apr 12 18:39:19 2012 +0200
    15.3 @@ -230,7 +230,9 @@
    15.4  use "Tools/holcf_library.ML"
    15.5  use "Tools/fixrec.ML"
    15.6  
    15.7 -setup {* Fixrec.setup *}
    15.8 +method_setup fixrec_simp = {*
    15.9 +  Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
   15.10 +*} "pattern prover for fixrec constants"
   15.11  
   15.12  setup {*
   15.13    Fixrec.add_matchers

    16.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Apr 12 11:34:50 2012 +0200
    16.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Apr 12 18:39:19 2012 +0200
    16.3 @@ -12,7 +12,6 @@
    16.4      -> (bool * (Attrib.binding * string)) list -> local_theory -> local_theory
    16.5    val add_matchers: (string * string) list -> theory -> theory
    16.6    val fixrec_simp_tac: Proof.context -> int -> tactic
    16.7 -  val setup: theory -> theory
    16.8  end
    16.9  
   16.10  structure Fixrec : FIXREC =
   16.11 @@ -406,9 +405,4 @@
   16.12      (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
   16.13        >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
   16.14  
   16.15 -val setup =
   16.16 -  Method.setup @{binding fixrec_simp}
   16.17 -    (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))
   16.18 -    "pattern prover for fixrec constants"
   16.19 -
   16.20  end

    17.1 --- a/src/HOL/Library/Countable.thy	Thu Apr 12 11:34:50 2012 +0200
    17.2 +++ b/src/HOL/Library/Countable.thy	Thu Apr 12 18:39:19 2012 +0200
    17.3 @@ -269,8 +269,7 @@
    17.4      by - (rule exI)
    17.5  qed
    17.6  
    17.7 -method_setup countable_datatype = {*
    17.8 -let
    17.9 +ML {*
   17.10    fun countable_tac ctxt =
   17.11      SUBGOAL (fn (goal, i) =>
   17.12        let
   17.13 @@ -297,9 +296,10 @@
   17.14             etac induct_thm i,
   17.15             REPEAT (resolve_tac rules i ORELSE atac i)]) 1
   17.16        end)
   17.17 -in
   17.18 +*}
   17.19 +
   17.20 +method_setup countable_datatype = {*
   17.21    Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt))
   17.22 -end
   17.23  *} "prove countable class instances for datatypes"
   17.24  
   17.25  hide_const (open) finite_item nth_item

    18.1 --- a/src/HOL/Library/Eval_Witness.thy	Thu Apr 12 11:34:50 2012 +0200
    18.2 +++ b/src/HOL/Library/Eval_Witness.thy	Thu Apr 12 18:39:19 2012 +0200
    18.3 @@ -77,8 +77,8 @@
    18.4  
    18.5  method_setup eval_witness = {*
    18.6    Scan.lift (Scan.repeat Args.name) >>
    18.7 -  (fn ws => K (SIMPLE_METHOD'
    18.8 -    (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
    18.9 +    (fn ws => K (SIMPLE_METHOD'
   18.10 +      (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
   18.11  *} "evaluation with ML witnesses"
   18.12  
   18.13  

    19.1 --- a/src/HOL/Limits.thy	Thu Apr 12 11:34:50 2012 +0200
    19.2 +++ b/src/HOL/Limits.thy	Thu Apr 12 18:39:19 2012 +0200
    19.3 @@ -112,7 +112,8 @@
    19.4  qed
    19.5  
    19.6  ML {*
    19.7 -  fun ev_elim_tac ctxt thms thm = let
    19.8 +  fun eventually_elim_tac ctxt thms thm =
    19.9 +    let
   19.10        val thy = Proof_Context.theory_of ctxt
   19.11        val mp_thms = thms RL [@{thm eventually_rev_mp}]
   19.12        val raw_elim_thm =
   19.13 @@ -124,13 +125,11 @@
   19.14      in
   19.15        CASES cases (rtac raw_elim_thm 1) thm
   19.16      end
   19.17 -
   19.18 -  fun eventually_elim_setup name =
   19.19 -    Method.setup name (Scan.succeed (fn ctxt => METHOD_CASES (ev_elim_tac ctxt)))
   19.20 -      "elimination of eventually quantifiers"
   19.21  *}
   19.22  
   19.23 -setup {* eventually_elim_setup @{binding "eventually_elim"} *}
   19.24 +method_setup eventually_elim = {*
   19.25 +  Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
   19.26 +*} "elimination of eventually quantifiers"
   19.27  
   19.28  
   19.29  subsection {* Finer-than relation *}

    20.1 --- a/src/HOL/NSA/StarDef.thy	Thu Apr 12 11:34:50 2012 +0200
    20.2 +++ b/src/HOL/NSA/StarDef.thy	Thu Apr 12 18:39:19 2012 +0200
    20.3 @@ -91,6 +91,12 @@
    20.4  use "transfer.ML"
    20.5  setup Transfer_Principle.setup
    20.6  
    20.7 +method_setup transfer = {*
    20.8 +  Attrib.thms >> (fn ths => fn ctxt =>
    20.9 +    SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))
   20.10 +*} "transfer principle"
   20.11 +
   20.12 +
   20.13  text {* Transfer introduction rules. *}
   20.14  
   20.15  lemma transfer_ex [transfer_intro]:

    21.1 --- a/src/HOL/NSA/transfer.ML	Thu Apr 12 11:34:50 2012 +0200
    21.2 +++ b/src/HOL/NSA/transfer.ML	Thu Apr 12 18:39:19 2012 +0200
    21.3 @@ -112,8 +112,6 @@
    21.4    Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
    21.5      "declaration of transfer unfolding rule" #>
    21.6    Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
    21.7 -    "declaration of transfer refolding rule" #>
    21.8 -  Method.setup @{binding transfer} (Attrib.thms >> (fn ths => fn ctxt =>
    21.9 -    SIMPLE_METHOD' (transfer_tac ctxt ths))) "transfer principle";
   21.10 +    "declaration of transfer refolding rule"
   21.11  
   21.12  end;

    22.1 --- a/src/HOL/Orderings.thy	Thu Apr 12 11:34:50 2012 +0200
    22.2 +++ b/src/HOL/Orderings.thy	Thu Apr 12 18:39:19 2012 +0200
    22.3 @@ -312,7 +312,7 @@
    22.4  signature ORDERS =
    22.5  sig
    22.6    val print_structures: Proof.context -> unit
    22.7 -  val setup: theory -> theory
    22.8 +  val attrib_setup: theory -> theory
    22.9    val order_tac: Proof.context -> thm list -> int -> tactic
   22.10  end;
   22.11  
   22.12 @@ -414,19 +414,15 @@
   22.13      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   22.14          Toplevel.keep (print_structures o Toplevel.context_of)));
   22.15  
   22.16 -
   22.17 -(** Setup **)
   22.18 -
   22.19 -val setup =
   22.20 -  Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt [])))
   22.21 -    "transitivity reasoner" #>
   22.22 -  attrib_setup;
   22.23 -
   22.24  end;
   22.25  
   22.26  *}
   22.27  
   22.28 -setup Orders.setup
   22.29 +setup Orders.attrib_setup
   22.30 +
   22.31 +method_setup order = {*
   22.32 +  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
   22.33 +*} "transitivity reasoner"
   22.34  
   22.35  
   22.36  text {* Declarations to set up transitivity reasoner of partial and linear orders. *}

    23.1 --- a/src/HOL/Presburger.thy	Thu Apr 12 11:34:50 2012 +0200
    23.2 +++ b/src/HOL/Presburger.thy	Thu Apr 12 18:39:19 2012 +0200
    23.3 @@ -387,10 +387,25 @@
    23.4    by (simp cong: conj_cong)
    23.5  
    23.6  use "Tools/Qelim/cooper.ML"
    23.7 -
    23.8  setup Cooper.setup
    23.9  
   23.10 -method_setup presburger = "Cooper.method" "Cooper's algorithm for Presburger arithmetic"
   23.11 +method_setup presburger = {*
   23.12 +  let
   23.13 +    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   23.14 +    fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
   23.15 +    val addN = "add"
   23.16 +    val delN = "del"
   23.17 +    val elimN = "elim"
   23.18 +    val any_keyword = keyword addN || keyword delN || simple_keyword elimN
   23.19 +    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   23.20 +  in
   23.21 +    Scan.optional (simple_keyword elimN >> K false) true --
   23.22 +    Scan.optional (keyword addN |-- thms) [] --
   23.23 +    Scan.optional (keyword delN |-- thms) [] >>
   23.24 +    (fn ((elim, add_ths), del_ths) => fn ctxt =>
   23.25 +      SIMPLE_METHOD' (Cooper.tac elim add_ths del_ths ctxt))
   23.26 +  end
   23.27 +*} "Cooper's algorithm for Presburger arithmetic"
   23.28  
   23.29  declare dvd_eq_mod_eq_0[symmetric, presburger]
   23.30  declare mod_1[presburger] 

    24.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Thu Apr 12 11:34:50 2012 +0200
    24.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Apr 12 18:39:19 2012 +0200
    24.3 @@ -9,7 +9,6 @@
    24.4    val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
    24.5                     -> Proof.context -> thm list -> tactic
    24.6    val induction_schema_tac : Proof.context -> thm list -> tactic
    24.7 -  val setup : theory -> theory
    24.8  end
    24.9  
   24.10  
   24.11 @@ -395,8 +394,4 @@
   24.12  fun induction_schema_tac ctxt =
   24.13    mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
   24.14  
   24.15 -val setup =
   24.16 -  Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac))
   24.17 -    "proves an induction principle"
   24.18 -
   24.19  end

    25.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Apr 12 11:34:50 2012 +0200
    25.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Apr 12 18:39:19 2012 +0200
    25.3 @@ -9,8 +9,6 @@
    25.4  sig
    25.5    val lex_order_tac : bool -> Proof.context -> tactic -> tactic
    25.6    val lexicographic_order_tac : bool -> Proof.context -> tactic
    25.7 -  val lexicographic_order : Proof.context -> Proof.method
    25.8 -
    25.9    val setup: theory -> theory
   25.10  end
   25.11  
   25.12 @@ -218,12 +216,7 @@
   25.13    lex_order_tac quiet ctxt
   25.14      (auto_tac (map_simpset (fn ss => ss addsimps Function_Common.Termination_Simps.get ctxt) ctxt))
   25.15  
   25.16 -val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
   25.17 -
   25.18  val setup =
   25.19 -  Method.setup @{binding lexicographic_order}
   25.20 -    (Method.sections clasimp_modifiers >> (K lexicographic_order))
   25.21 -    "termination prover for lexicographic orderings"
   25.22 -  #> Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
   25.23 +  Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false))
   25.24  
   25.25  end;

    26.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Thu Apr 12 11:34:50 2012 +0200
    26.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Thu Apr 12 18:39:19 2012 +0200
    26.3 @@ -7,11 +7,8 @@
    26.4  signature PAT_COMPLETENESS =
    26.5  sig
    26.6      val pat_completeness_tac: Proof.context -> int -> tactic
    26.7 -    val pat_completeness: Proof.context -> Proof.method
    26.8      val prove_completeness : theory -> term list -> term -> term list list ->
    26.9        term list list -> thm
   26.10 -
   26.11 -    val setup : theory -> theory
   26.12  end
   26.13  
   26.14  structure Pat_Completeness : PAT_COMPLETENESS =
   26.15 @@ -153,11 +150,4 @@
   26.16    end
   26.17    handle COMPLETENESS => no_tac)
   26.18  
   26.19 -
   26.20 -val pat_completeness = SIMPLE_METHOD' o pat_completeness_tac
   26.21 -
   26.22 -val setup =
   26.23 -  Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
   26.24 -    "Completeness prover for datatype patterns"
   26.25 -
   26.26  end

    27.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Apr 12 11:34:50 2012 +0200
    27.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Apr 12 18:39:19 2012 +0200
    27.3 @@ -13,7 +13,6 @@
    27.4    exception COOPER of string
    27.5    val conv: Proof.context -> conv
    27.6    val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
    27.7 -  val method: (Proof.context -> Method.method) context_parser
    27.8    val setup: theory -> theory
    27.9  end;
   27.10  
   27.11 @@ -857,23 +856,6 @@
   27.12    THEN_ALL_NEW finish_tac elim
   27.13  end;
   27.14  
   27.15 -val method =
   27.16 -  let
   27.17 -    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   27.18 -    fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
   27.19 -    val addN = "add"
   27.20 -    val delN = "del"
   27.21 -    val elimN = "elim"
   27.22 -    val any_keyword = keyword addN || keyword delN || simple_keyword elimN
   27.23 -    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   27.24 -  in
   27.25 -    Scan.optional (simple_keyword elimN >> K false) true --
   27.26 -    Scan.optional (keyword addN |-- thms) [] --
   27.27 -    Scan.optional (keyword delN |-- thms) [] >>
   27.28 -    (fn ((elim, add_ths), del_ths) => fn ctxt =>
   27.29 -      SIMPLE_METHOD' (tac elim add_ths del_ths ctxt))
   27.30 -  end;
   27.31 -
   27.32  
   27.33  (* theory setup *)
   27.34  

    28.1 --- a/src/HOL/Tools/groebner.ML	Thu Apr 12 11:34:50 2012 +0200
    28.2 +++ b/src/HOL/Tools/groebner.ML	Thu Apr 12 18:39:19 2012 +0200
    28.3 @@ -16,7 +16,6 @@
    28.4    val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
    28.5    val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
    28.6    val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
    28.7 -  val algebra_method: (Proof.context -> Method.method) context_parser
    28.8  end
    28.9  
   28.10  structure Groebner : GROEBNER =
   28.11 @@ -1027,21 +1026,4 @@
   28.12  fun algebra_tac add_ths del_ths ctxt i =
   28.13   ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
   28.14  
   28.15 -local
   28.16 -
   28.17 -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   28.18 -val addN = "add"
   28.19 -val delN = "del"
   28.20 -val any_keyword = keyword addN || keyword delN
   28.21 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   28.22 -
   28.23 -in
   28.24 -
   28.25 -val algebra_method = ((Scan.optional (keyword addN |-- thms) []) --
   28.26 -   (Scan.optional (keyword delN |-- thms) [])) >>
   28.27 -  (fn (add_ths, del_ths) => fn ctxt =>
   28.28 -       SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt))
   28.29 -
   28.30  end;
   28.31 -
   28.32 -end;

    29.1 --- a/src/HOL/ex/SAT_Examples.thy	Thu Apr 12 11:34:50 2012 +0200
    29.2 +++ b/src/HOL/ex/SAT_Examples.thy	Thu Apr 12 18:39:19 2012 +0200
    29.3 @@ -80,11 +80,9 @@
    29.4  ML {* sat.trace_sat := false; *}
    29.5  ML {* quick_and_dirty := false; *}
    29.6  
    29.7 -method_setup rawsat =
    29.8 -  {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}
    29.9 -  "SAT solver (no preprocessing)"
   29.10 -
   29.11 -(* ML {* Toplevel.profiling := 1; *} *)
   29.12 +method_setup rawsat = {*
   29.13 +  Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
   29.14 +*} "SAT solver (no preprocessing)"
   29.15  
   29.16  (* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
   29.17  
   29.18 @@ -512,8 +510,6 @@
   29.19     (as of 2006-08-30, on a 2.5 GHz Pentium 4)
   29.20  *)
   29.21  
   29.22 -(* ML {* Toplevel.profiling := 0; *} *)
   29.23 -
   29.24  text {*
   29.25  Function {\tt benchmark} takes the name of an existing DIMACS CNF
   29.26  file, parses this file, passes the problem to a SAT solver, and checks