unified type Proof.method and pervasive METHOD combinators;
authorwenzelm
Fri Mar 13 19:58:26 2009 +0100 (2009-03-13)
changeset 305104120fc59dd85
parent 30509 e19d5b459a61
child 30511 5c628a39b7cb
unified type Proof.method and pervasive METHOD combinators;
doc-src/IsarRef/Thy/Proof.thy
doc-src/IsarRef/Thy/document/Proof.tex
doc-src/TutorialI/Protocol/Event.thy
src/CCL/Wfd.thy
src/Cube/Example.thy
src/FOL/ex/Iff_Oracle.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/ringsimp.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/OtwayReesBella.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Smartcard/ShoupRubin.thy
src/HOL/Auth/Smartcard/ShoupRubinBella.thy
src/HOL/Auth/Smartcard/Smartcard.thy
src/HOL/Code_Setup.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Groebner_Basis.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/HoareParallel/OG_Tactics.thy
src/HOL/Import/import_package.ML
src/HOL/Import/shuffler.ML
src/HOL/Isar_examples/Hoare.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/Reflection.thy
src/HOL/Library/Topology_Euclidean_Space.thy
src/HOL/Library/comm_ring.ML
src/HOL/NSA/transfer.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Orderings.thy
src/HOL/Presburger.thy
src/HOL/Prolog/HOHH.thy
src/HOL/SAT.thy
src/HOL/SET-Protocol/EventSET.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/SET-Protocol/PublicSET.thy
src/HOL/Statespace/state_space.ML
src/HOL/Tools/function_package/auto_term.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/induction_scheme.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/scnp_reconstruct.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/ex/Binary.thy
src/HOL/ex/SAT_Examples.thy
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/hypsubst.ML
src/Provers/splitter.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/element.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_insts.ML
src/Pure/simplifier.ML
src/Sequents/ILL.thy
src/Sequents/LK0.thy
src/Sequents/S4.thy
src/Sequents/S43.thy
src/Sequents/T.thy
src/Tools/atomize_elim.ML
src/Tools/coherent.ML
src/Tools/eqsubst.ML
src/Tools/induct.ML
src/Tools/intuitionistic.ML
src/ZF/Tools/typechk.ML
src/ZF/UNITY/Constrains.thy
     1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -895,11 +895,10 @@
     1.4  %FIXME proper antiquotations
     1.5  {\footnotesize
     1.6  \begin{verbatim}
     1.7 - Method.no_args (Method.METHOD (fn facts => foobar_tac))
     1.8 - Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
     1.9 - Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
    1.10 - Method.thms_ctxt_args (fn thms => fn ctxt =>
    1.11 -    Method.METHOD (fn facts => foobar_tac))
    1.12 + Method.no_args (METHOD (fn facts => foobar_tac))
    1.13 + Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
    1.14 + Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
    1.15 + Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac))
    1.16  \end{verbatim}
    1.17  }
    1.18  
     2.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Fri Mar 13 19:53:09 2009 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Mar 13 19:58:26 2009 +0100
     2.3 @@ -899,11 +899,10 @@
     2.4  %FIXME proper antiquotations
     2.5  {\footnotesize
     2.6  \begin{verbatim}
     2.7 - Method.no_args (Method.METHOD (fn facts => foobar_tac))
     2.8 - Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
     2.9 - Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
    2.10 - Method.thms_ctxt_args (fn thms => fn ctxt =>
    2.11 -    Method.METHOD (fn facts => foobar_tac))
    2.12 + Method.no_args (METHOD (fn facts => foobar_tac))
    2.13 + Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
    2.14 + Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
    2.15 + Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac))
    2.16  \end{verbatim}
    2.17  }
    2.18  
     3.1 --- a/doc-src/TutorialI/Protocol/Event.thy	Fri Mar 13 19:53:09 2009 +0100
     3.2 +++ b/doc-src/TutorialI/Protocol/Event.thy	Fri Mar 13 19:58:26 2009 +0100
     3.3 @@ -287,7 +287,7 @@
     3.4      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
     3.5  
     3.6  method_setup analz_mono_contra = {*
     3.7 -    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     3.8 +    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     3.9      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    3.10  
    3.11  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    3.12 @@ -344,7 +344,7 @@
    3.13  *}
    3.14  
    3.15  method_setup synth_analz_mono_contra = {*
    3.16 -    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    3.17 +    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    3.18      "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
    3.19  (*>*)
    3.20  
     4.1 --- a/src/CCL/Wfd.thy	Fri Mar 13 19:53:09 2009 +0100
     4.2 +++ b/src/CCL/Wfd.thy	Fri Mar 13 19:58:26 2009 +0100
     4.3 @@ -505,7 +505,7 @@
     4.4  val eval_setup =
     4.5    Data.setup #>
     4.6    Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
     4.7 -    Method.SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")];
     4.8 +    SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")];
     4.9  
    4.10  end;
    4.11  
     5.1 --- a/src/Cube/Example.thy	Fri Mar 13 19:53:09 2009 +0100
     5.2 +++ b/src/Cube/Example.thy	Fri Mar 13 19:58:26 2009 +0100
     5.3 @@ -15,18 +15,18 @@
     5.4  *}
     5.5  
     5.6  method_setup depth_solve = {*
     5.7 -  Method.thms_args (fn thms => Method.METHOD (fn facts =>
     5.8 +  Method.thms_args (fn thms => METHOD (fn facts =>
     5.9    (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
    5.10  *} ""
    5.11  
    5.12  method_setup depth_solve1 = {*
    5.13 -  Method.thms_args (fn thms => Method.METHOD (fn facts =>
    5.14 +  Method.thms_args (fn thms => METHOD (fn facts =>
    5.15    (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
    5.16  *} ""
    5.17  
    5.18  method_setup strip_asms =  {*
    5.19    let val strip_b = thm "strip_b" and strip_s = thm "strip_s" in
    5.20 -    Method.thms_args (fn thms => Method.METHOD (fn facts =>
    5.21 +    Method.thms_args (fn thms => METHOD (fn facts =>
    5.22        REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
    5.23    end
    5.24  *} ""
     6.1 --- a/src/FOL/ex/Iff_Oracle.thy	Fri Mar 13 19:53:09 2009 +0100
     6.2 +++ b/src/FOL/ex/Iff_Oracle.thy	Fri Mar 13 19:58:26 2009 +0100
     6.3 @@ -53,7 +53,7 @@
     6.4  
     6.5  method_setup iff = {*
     6.6    Method.simple_args OuterParse.nat (fn n => fn ctxt =>
     6.7 -    Method.SIMPLE_METHOD
     6.8 +    SIMPLE_METHOD
     6.9        (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
    6.10          handle Fail _ => no_tac))
    6.11  *} "iff oracle"
     7.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Fri Mar 13 19:53:09 2009 +0100
     7.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri Mar 13 19:58:26 2009 +0100
     7.3 @@ -222,7 +222,7 @@
     7.4  *}   (* Note: r_one is not necessary in ring_ss *)
     7.5  
     7.6  method_setup ring =
     7.7 -  {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
     7.8 +  {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
     7.9    {* computes distributive normal form in rings *}
    7.10  
    7.11  
     8.1 --- a/src/HOL/Algebra/ringsimp.ML	Fri Mar 13 19:53:09 2009 +0100
     8.2 +++ b/src/HOL/Algebra/ringsimp.ML	Fri Mar 13 19:58:26 2009 +0100
     8.3 @@ -72,7 +72,7 @@
     8.4  (** Setup **)
     8.5  
     8.6  val setup =
     8.7 -  Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac),
     8.8 +  Method.add_methods [("algebra", Method.ctxt_args (SIMPLE_METHOD' o algebra_tac),
     8.9      "normalisation of algebraic structure")] #>
    8.10    Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
    8.11  
     9.1 --- a/src/HOL/Auth/Event.thy	Fri Mar 13 19:53:09 2009 +0100
     9.2 +++ b/src/HOL/Auth/Event.thy	Fri Mar 13 19:58:26 2009 +0100
     9.3 @@ -289,7 +289,7 @@
     9.4  *}
     9.5  
     9.6  method_setup analz_mono_contra = {*
     9.7 -    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     9.8 +    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     9.9      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    9.10  
    9.11  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    9.12 @@ -310,7 +310,7 @@
    9.13  *}
    9.14  
    9.15  method_setup synth_analz_mono_contra = {*
    9.16 -    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    9.17 +    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    9.18      "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
    9.19  
    9.20  end
    10.1 --- a/src/HOL/Auth/Message.thy	Fri Mar 13 19:53:09 2009 +0100
    10.2 +++ b/src/HOL/Auth/Message.thy	Fri Mar 13 19:58:26 2009 +0100
    10.3 @@ -941,18 +941,15 @@
    10.4  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
    10.5  
    10.6  method_setup spy_analz = {*
    10.7 -    Method.ctxt_args (fn ctxt =>
    10.8 -        Method.SIMPLE_METHOD (Message.gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    10.9 +    Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
   10.10      "for proving the Fake case when analz is involved"
   10.11  
   10.12  method_setup atomic_spy_analz = {*
   10.13 -    Method.ctxt_args (fn ctxt =>
   10.14 -        Method.SIMPLE_METHOD (Message.atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
   10.15 +    Method.ctxt_args (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
   10.16      "for debugging spy_analz"
   10.17  
   10.18  method_setup Fake_insert_simp = {*
   10.19 -    Method.ctxt_args (fn ctxt =>
   10.20 -        Method.SIMPLE_METHOD (Message.Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
   10.21 +    Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
   10.22      "for debugging spy_analz"
   10.23  
   10.24  end
    11.1 --- a/src/HOL/Auth/OtwayReesBella.thy	Fri Mar 13 19:53:09 2009 +0100
    11.2 +++ b/src/HOL/Auth/OtwayReesBella.thy	Fri Mar 13 19:58:26 2009 +0100
    11.3 @@ -137,7 +137,7 @@
    11.4  *}
    11.5   
    11.6  method_setup parts_explicit = {*
    11.7 -    Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *}
    11.8 +    Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *}
    11.9    "to explicitly state that some message components belong to parts knows Spy"
   11.10  
   11.11  
   11.12 @@ -258,7 +258,7 @@
   11.13  
   11.14  method_setup analz_freshCryptK = {*
   11.15      Method.ctxt_args (fn ctxt =>
   11.16 -     (Method.SIMPLE_METHOD
   11.17 +     (SIMPLE_METHOD
   11.18        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   11.19            REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
   11.20            ALLGOALS (asm_simp_tac
   11.21 @@ -268,7 +268,7 @@
   11.22  
   11.23  method_setup disentangle = {*
   11.24      Method.no_args
   11.25 -     (Method.SIMPLE_METHOD
   11.26 +     (SIMPLE_METHOD
   11.27        (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
   11.28                     ORELSE' hyp_subst_tac))) *}
   11.29    "for eliminating conjunctions, disjunctions and the like"
    12.1 --- a/src/HOL/Auth/Public.thy	Fri Mar 13 19:53:09 2009 +0100
    12.2 +++ b/src/HOL/Auth/Public.thy	Fri Mar 13 19:58:26 2009 +0100
    12.3 @@ -425,7 +425,7 @@
    12.4  
    12.5  method_setup analz_freshK = {*
    12.6      Method.ctxt_args (fn ctxt =>
    12.7 -     (Method.SIMPLE_METHOD
    12.8 +     (SIMPLE_METHOD
    12.9        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   12.10            REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   12.11            ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *}
   12.12 @@ -435,13 +435,11 @@
   12.13  subsection{*Specialized Methods for Possibility Theorems*}
   12.14  
   12.15  method_setup possibility = {*
   12.16 -    Method.ctxt_args (fn ctxt =>
   12.17 -        Method.SIMPLE_METHOD (Public.possibility_tac ctxt)) *}
   12.18 +    Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *}
   12.19      "for proving possibility theorems"
   12.20  
   12.21  method_setup basic_possibility = {*
   12.22 -    Method.ctxt_args (fn ctxt =>
   12.23 -        Method.SIMPLE_METHOD (Public.basic_possibility_tac ctxt)) *}
   12.24 +    Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *}
   12.25      "for proving possibility theorems"
   12.26  
   12.27  end
    13.1 --- a/src/HOL/Auth/Shared.thy	Fri Mar 13 19:53:09 2009 +0100
    13.2 +++ b/src/HOL/Auth/Shared.thy	Fri Mar 13 19:58:26 2009 +0100
    13.3 @@ -239,20 +239,18 @@
    13.4  
    13.5  method_setup analz_freshK = {*
    13.6      Method.ctxt_args (fn ctxt =>
    13.7 -     (Method.SIMPLE_METHOD
    13.8 +     (SIMPLE_METHOD
    13.9        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   13.10            REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   13.11            ALLGOALS (asm_simp_tac (Simplifier.context ctxt Shared.analz_image_freshK_ss))]))) *}
   13.12      "for proving the Session Key Compromise theorem"
   13.13  
   13.14  method_setup possibility = {*
   13.15 -    Method.ctxt_args (fn ctxt =>
   13.16 -        Method.SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
   13.17 +    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
   13.18      "for proving possibility theorems"
   13.19  
   13.20  method_setup basic_possibility = {*
   13.21 -    Method.ctxt_args (fn ctxt =>
   13.22 -        Method.SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
   13.23 +    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
   13.24      "for proving possibility theorems"
   13.25  
   13.26  lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
    14.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri Mar 13 19:53:09 2009 +0100
    14.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri Mar 13 19:58:26 2009 +0100
    14.3 @@ -769,15 +769,15 @@
    14.4  *}
    14.5  
    14.6  method_setup prepare = {*
    14.7 -    Method.no_args (Method.SIMPLE_METHOD ShoupRubin.prepare_tac) *}
    14.8 +    Method.no_args (SIMPLE_METHOD ShoupRubin.prepare_tac) *}
    14.9    "to launch a few simple facts that'll help the simplifier"
   14.10  
   14.11  method_setup parts_prepare = {*
   14.12 -    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
   14.13 +    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
   14.14    "additional facts to reason about parts"
   14.15  
   14.16  method_setup analz_prepare = {*
   14.17 -    Method.no_args (Method.SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
   14.18 +    Method.no_args (SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
   14.19    "additional facts to reason about analz"
   14.20  
   14.21  
   14.22 @@ -823,7 +823,7 @@
   14.23  
   14.24  method_setup sc_analz_freshK = {*
   14.25      Method.ctxt_args (fn ctxt =>
   14.26 -     (Method.SIMPLE_METHOD
   14.27 +     (SIMPLE_METHOD
   14.28        (EVERY [REPEAT_FIRST
   14.29         (resolve_tac [allI, ballI, impI]),
   14.30          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
    15.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Fri Mar 13 19:53:09 2009 +0100
    15.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Fri Mar 13 19:58:26 2009 +0100
    15.3 @@ -777,15 +777,15 @@
    15.4  *}
    15.5  
    15.6  method_setup prepare = {*
    15.7 -    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
    15.8 +    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
    15.9    "to launch a few simple facts that'll help the simplifier"
   15.10  
   15.11  method_setup parts_prepare = {*
   15.12 -    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
   15.13 +    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
   15.14    "additional facts to reason about parts"
   15.15  
   15.16  method_setup analz_prepare = {*
   15.17 -    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
   15.18 +    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
   15.19    "additional facts to reason about analz"
   15.20  
   15.21  
   15.22 @@ -832,7 +832,7 @@
   15.23  
   15.24  method_setup sc_analz_freshK = {*
   15.25      Method.ctxt_args (fn ctxt =>
   15.26 -     (Method.SIMPLE_METHOD
   15.27 +     (SIMPLE_METHOD
   15.28        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   15.29            REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   15.30            ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss
    16.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Mar 13 19:53:09 2009 +0100
    16.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Mar 13 19:58:26 2009 +0100
    16.3 @@ -408,7 +408,7 @@
    16.4  
    16.5  method_setup analz_freshK = {*
    16.6      Method.ctxt_args (fn ctxt =>
    16.7 -     (Method.SIMPLE_METHOD
    16.8 +     (SIMPLE_METHOD
    16.9        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   16.10            REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   16.11            ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss))]))) *}
   16.12 @@ -416,12 +416,12 @@
   16.13  
   16.14  method_setup possibility = {*
   16.15      Method.ctxt_args (fn ctxt =>
   16.16 -        Method.SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
   16.17 +        SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
   16.18      "for proving possibility theorems"
   16.19  
   16.20  method_setup basic_possibility = {*
   16.21      Method.ctxt_args (fn ctxt =>
   16.22 -        Method.SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
   16.23 +        SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
   16.24      "for proving possibility theorems"
   16.25  
   16.26  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
    17.1 --- a/src/HOL/Code_Setup.thy	Fri Mar 13 19:53:09 2009 +0100
    17.2 +++ b/src/HOL/Code_Setup.thy	Fri Mar 13 19:58:26 2009 +0100
    17.3 @@ -226,7 +226,7 @@
    17.4  *}
    17.5  
    17.6  ML {*
    17.7 -fun gen_eval_method conv = Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD'
    17.8 +fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD'
    17.9    (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
   17.10      THEN' rtac TrueI))
   17.11  *}
   17.12 @@ -237,7 +237,7 @@
   17.13  method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
   17.14    "solve goal by evaluation"
   17.15  
   17.16 -method_setup normalization = {* (Method.no_args o Method.SIMPLE_METHOD')
   17.17 +method_setup normalization = {* (Method.no_args o SIMPLE_METHOD')
   17.18    (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
   17.19  *} "solve goal by normalization"
   17.20  
    18.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Mar 13 19:53:09 2009 +0100
    18.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Mar 13 19:58:26 2009 +0100
    18.3 @@ -2499,7 +2499,7 @@
    18.4  method_setup approximation = {* fn src => 
    18.5    Method.syntax Args.term src #>
    18.6    (fn (prec, ctxt) => let
    18.7 -   in Method.SIMPLE_METHOD' (fn i =>
    18.8 +   in SIMPLE_METHOD' (fn i =>
    18.9       (DETERM (reify_uneq ctxt i)
   18.10        THEN rule_uneq ctxt prec i
   18.11        THEN Simplifier.asm_full_simp_tac bounded_by_simpset i 
    19.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 13 19:53:09 2009 +0100
    19.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 13 19:58:26 2009 +0100
    19.3 @@ -295,7 +295,7 @@
    19.4  
    19.5  use "~~/src/HOL/Tools/Qelim/langford.ML"
    19.6  method_setup dlo = {*
    19.7 -  Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
    19.8 +  Method.ctxt_args (SIMPLE_METHOD' o LangfordQE.dlo_tac)
    19.9  *} "Langford's algorithm for quantifier elimination in dense linear orders"
   19.10  
   19.11  
   19.12 @@ -546,7 +546,7 @@
   19.13  use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML"
   19.14  
   19.15  method_setup ferrack = {*
   19.16 -  Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
   19.17 +  Method.ctxt_args (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
   19.18  *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
   19.19  
   19.20  subsection {* Ferrante and Rackoff algorithm over ordered fields *}
    20.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 13 19:53:09 2009 +0100
    20.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 13 19:58:26 2009 +0100
    20.3 @@ -100,7 +100,7 @@
    20.4  
    20.5  fun linr_meth src =
    20.6    Method.syntax (Args.mode "no_quantify") src
    20.7 -  #> (fn (q, ctxt) => Method.SIMPLE_METHOD' (linr_tac ctxt (not q)));
    20.8 +  #> (fn (q, ctxt) => SIMPLE_METHOD' (linr_tac ctxt (not q)));
    20.9  
   20.10  val setup =
   20.11    Method.add_method ("rferrack", linr_meth,
    21.1 --- a/src/HOL/Groebner_Basis.thy	Fri Mar 13 19:53:09 2009 +0100
    21.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Mar 13 19:58:26 2009 +0100
    21.3 @@ -253,7 +253,7 @@
    21.4  
    21.5  
    21.6  method_setup sring_norm = {*
    21.7 -  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
    21.8 +  Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
    21.9  *} "semiring normalizer"
   21.10  
   21.11  
   21.12 @@ -431,7 +431,7 @@
   21.13      ((Scan.optional (keyword addN |-- thms) []) -- 
   21.14      (Scan.optional (keyword delN |-- thms) [])) src 
   21.15   #> (fn ((add_ths, del_ths), ctxt) => 
   21.16 -       Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
   21.17 +       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
   21.18  end
   21.19  *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
   21.20  declare dvd_def[algebra]
    22.1 --- a/src/HOL/Hoare/Hoare.thy	Fri Mar 13 19:53:09 2009 +0100
    22.2 +++ b/src/HOL/Hoare/Hoare.thy	Fri Mar 13 19:58:26 2009 +0100
    22.3 @@ -234,12 +234,12 @@
    22.4  use "hoare_tac.ML"
    22.5  
    22.6  method_setup vcg = {*
    22.7 -  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    22.8 +  Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    22.9    "verification condition generator"
   22.10  
   22.11  method_setup vcg_simp = {*
   22.12    Method.ctxt_args (fn ctxt =>
   22.13 -    Method.SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   22.14 +    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   22.15    "verification condition generator plus simplification"
   22.16  
   22.17  end
    23.1 --- a/src/HOL/Hoare/HoareAbort.thy	Fri Mar 13 19:53:09 2009 +0100
    23.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Fri Mar 13 19:58:26 2009 +0100
    23.3 @@ -246,12 +246,12 @@
    23.4  use "hoare_tac.ML"
    23.5  
    23.6  method_setup vcg = {*
    23.7 -  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    23.8 +  Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    23.9    "verification condition generator"
   23.10  
   23.11  method_setup vcg_simp = {*
   23.12    Method.ctxt_args (fn ctxt =>
   23.13 -    Method.SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   23.14 +    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   23.15    "verification condition generator plus simplification"
   23.16  
   23.17  (* Special syntax for guarded statements and guarded array updates: *)
    24.1 --- a/src/HOL/HoareParallel/OG_Tactics.thy	Fri Mar 13 19:53:09 2009 +0100
    24.2 +++ b/src/HOL/HoareParallel/OG_Tactics.thy	Fri Mar 13 19:58:26 2009 +0100
    24.3 @@ -465,21 +465,21 @@
    24.4  Isabelle proofs. *}
    24.5  
    24.6  method_setup oghoare = {*
    24.7 -  Method.no_args (Method.SIMPLE_METHOD' oghoare_tac) *}
    24.8 +  Method.no_args (SIMPLE_METHOD' oghoare_tac) *}
    24.9    "verification condition generator for the oghoare logic"
   24.10  
   24.11  method_setup annhoare = {*
   24.12 -  Method.no_args (Method.SIMPLE_METHOD' annhoare_tac) *}
   24.13 +  Method.no_args (SIMPLE_METHOD' annhoare_tac) *}
   24.14    "verification condition generator for the ann_hoare logic"
   24.15  
   24.16  method_setup interfree_aux = {*
   24.17 -  Method.no_args (Method.SIMPLE_METHOD' interfree_aux_tac) *}
   24.18 +  Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *}
   24.19    "verification condition generator for interference freedom tests"
   24.20  
   24.21  text {* Tactics useful for dealing with the generated verification conditions: *}
   24.22  
   24.23  method_setup conjI_tac = {*
   24.24 -  Method.no_args (Method.SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
   24.25 +  Method.no_args (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
   24.26    "verification condition generator for interference freedom tests"
   24.27  
   24.28  ML {*
   24.29 @@ -490,7 +490,7 @@
   24.30  *}
   24.31  
   24.32  method_setup disjE_tac = {*
   24.33 -  Method.no_args (Method.SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
   24.34 +  Method.no_args (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
   24.35    "verification condition generator for interference freedom tests"
   24.36  
   24.37  end
    25.1 --- a/src/HOL/Import/import_package.ML	Fri Mar 13 19:53:09 2009 +0100
    25.2 +++ b/src/HOL/Import/import_package.ML	Fri Mar 13 19:58:26 2009 +0100
    25.3 @@ -73,7 +73,7 @@
    25.4                        let
    25.5                            val thy = ProofContext.theory_of ctxt
    25.6                        in
    25.7 -                          Method.SIMPLE_METHOD (import_tac arg thy)
    25.8 +                          SIMPLE_METHOD (import_tac arg thy)
    25.9                        end)
   25.10  
   25.11  val setup = Method.add_method("import",import_meth,"Import HOL4 theorem")
    26.1 --- a/src/HOL/Import/shuffler.ML	Fri Mar 13 19:53:09 2009 +0100
    26.2 +++ b/src/HOL/Import/shuffler.ML	Fri Mar 13 19:58:26 2009 +0100
    26.3 @@ -656,7 +656,7 @@
    26.4      let
    26.5          val thy = ProofContext.theory_of ctxt
    26.6      in
    26.7 -        Method.SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
    26.8 +        SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
    26.9      end
   26.10  
   26.11  fun search_meth ctxt =
   26.12 @@ -664,7 +664,7 @@
   26.13          val thy = ProofContext.theory_of ctxt
   26.14          val prems = Assumption.all_prems_of ctxt
   26.15      in
   26.16 -        Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
   26.17 +        SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
   26.18      end
   26.19  
   26.20  fun add_shuffle_rule thm thy =
    27.1 --- a/src/HOL/Isar_examples/Hoare.thy	Fri Mar 13 19:53:09 2009 +0100
    27.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Fri Mar 13 19:58:26 2009 +0100
    27.3 @@ -455,7 +455,7 @@
    27.4  
    27.5  method_setup hoare = {*
    27.6    Method.ctxt_args (fn ctxt =>
    27.7 -    (Method.SIMPLE_METHOD'
    27.8 +    (SIMPLE_METHOD'
    27.9         (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}
   27.10    "verification condition generator for Hoare logic"
   27.11  
    28.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Mar 13 19:53:09 2009 +0100
    28.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri Mar 13 19:58:26 2009 +0100
    28.3 @@ -134,7 +134,7 @@
    28.4     (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
    28.5     THEN' asm_full_simp_tac (ss2 addsimps ths)
    28.6   in
    28.7 -  Method.thms_args (Method.SIMPLE_METHOD' o vector_arith_tac)
    28.8 +  Method.thms_args (SIMPLE_METHOD' o vector_arith_tac)
    28.9  end
   28.10  *} "Lifts trivial vector statements to real arith statements"
   28.11  
   28.12 @@ -948,7 +948,7 @@
   28.13  
   28.14  use "normarith.ML"
   28.15  
   28.16 -method_setup norm = {* Method.ctxt_args (Method.SIMPLE_METHOD' o NormArith.norm_arith_tac)
   28.17 +method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
   28.18  *} "Proves simple linear statements about vector norms"
   28.19  
   28.20  
    29.1 --- a/src/HOL/Library/Eval_Witness.thy	Fri Mar 13 19:53:09 2009 +0100
    29.2 +++ b/src/HOL/Library/Eval_Witness.thy	Fri Mar 13 19:58:26 2009 +0100
    29.3 @@ -84,7 +84,7 @@
    29.4  
    29.5  in
    29.6    Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
    29.7 -    Method.SIMPLE_METHOD' (eval_tac ws))
    29.8 +    SIMPLE_METHOD' (eval_tac ws))
    29.9  end
   29.10  *} "Evaluation with ML witnesses"
   29.11  
    30.1 --- a/src/HOL/Library/Reflection.thy	Fri Mar 13 19:53:09 2009 +0100
    30.2 +++ b/src/HOL/Library/Reflection.thy	Fri Mar 13 19:58:26 2009 +0100
    30.3 @@ -19,7 +19,7 @@
    30.4  method_setup reify = {* fn src =>
    30.5    Method.syntax (Attrib.thms --
    30.6      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
    30.7 -  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
    30.8 +  (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
    30.9  *} "partial automatic reification"
   30.10  
   30.11  method_setup reflection = {* 
   30.12 @@ -38,7 +38,7 @@
   30.13          val (ceqs,cths) = Reify_Data.get ctxt 
   30.14          val corr_thms = ths@cths
   30.15          val raw_eqs = eqs@ceqs
   30.16 -      in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
   30.17 +      in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
   30.18       end) end
   30.19  *} "reflection method"
   30.20  
    31.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Mar 13 19:53:09 2009 +0100
    31.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Mar 13 19:58:26 2009 +0100
    31.3 @@ -978,7 +978,7 @@
    31.4    val ss1 = HOL_basic_ss addsimps [@{thm expand_fun_eq} RS sym]
    31.5    val ss2 = HOL_basic_ss addsimps [@{thm mknet_inverse'}]
    31.6    fun tac ths = ObjectLogic.full_atomize_tac THEN' Simplifier.simp_tac (ss1 addsimps ths) THEN' Simplifier.asm_full_simp_tac ss2
    31.7 -  in Method.thms_args (Method.SIMPLE_METHOD' o tac) end
    31.8 +  in Method.thms_args (SIMPLE_METHOD' o tac) end
    31.9  
   31.10  *} "Reduces goals about net"
   31.11  
    32.1 --- a/src/HOL/Library/comm_ring.ML	Fri Mar 13 19:53:09 2009 +0100
    32.2 +++ b/src/HOL/Library/comm_ring.ML	Fri Mar 13 19:58:26 2009 +0100
    32.3 @@ -101,7 +101,7 @@
    32.4    end);
    32.5  
    32.6  val comm_ring_meth =
    32.7 -  Method.ctxt_args (Method.SIMPLE_METHOD' o comm_ring_tac);
    32.8 +  Method.ctxt_args (SIMPLE_METHOD' o comm_ring_tac);
    32.9  
   32.10  val setup =
   32.11    Method.add_method ("comm_ring", comm_ring_meth,
    33.1 --- a/src/HOL/NSA/transfer.ML	Fri Mar 13 19:53:09 2009 +0100
    33.2 +++ b/src/HOL/NSA/transfer.ML	Fri Mar 13 19:58:26 2009 +0100
    33.3 @@ -116,6 +116,6 @@
    33.4       ("transfer_refold", Attrib.add_del_args refold_add refold_del,
    33.5        "declaration of transfer refolding rule")] #>
    33.6    Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt =>
    33.7 -    Method.SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
    33.8 +    SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
    33.9  
   33.10  end;
    34.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Mar 13 19:53:09 2009 +0100
    34.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Mar 13 19:58:26 2009 +0100
    34.3 @@ -204,4 +204,4 @@
    34.4  
    34.5  val setup_fresh_fun_simp =
    34.6    Method.simple_args options_syntax 
    34.7 -  (fn b => fn _ => Method.SIMPLE_METHOD (fresh_fun_tac b 1))
    34.8 +  (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1))
    35.1 --- a/src/HOL/Nominal/nominal_induct.ML	Fri Mar 13 19:53:09 2009 +0100
    35.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Fri Mar 13 19:58:26 2009 +0100
    35.3 @@ -8,7 +8,7 @@
    35.4    val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
    35.5      (string * typ) list -> (string * typ) list list -> thm list ->
    35.6      thm list -> int -> RuleCases.cases_tactic
    35.7 -  val nominal_induct_method: Method.src -> Proof.context -> Method.method
    35.8 +  val nominal_induct_method: Method.src -> Proof.context -> Proof.method
    35.9  end =
   35.10  struct
   35.11  
   35.12 @@ -157,7 +157,7 @@
   35.13     (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   35.14      avoiding -- fixing -- rule_spec) src
   35.15    #> (fn ((((x, y), z), w), ctxt) =>
   35.16 -    Method.RAW_METHOD_CASES (fn facts =>
   35.17 +    RAW_METHOD_CASES (fn facts =>
   35.18        HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
   35.19  
   35.20  end;
    36.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 13 19:53:09 2009 +0100
    36.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 13 19:58:26 2009 +0100
    36.3 @@ -400,7 +400,7 @@
    36.4    Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) ||
    36.5    Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
    36.6  
    36.7 -fun perm_simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
    36.8 +fun perm_simp_method (prems, tac) ctxt = METHOD (fn facts =>
    36.9     HEADGOAL (Method.insert_tac (prems @ facts) THEN'
   36.10         ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
   36.11  
   36.12 @@ -411,7 +411,7 @@
   36.13  (* setup so that the simpset is used which is active at the moment when the tactic is called *)
   36.14  fun local_simp_meth_setup tac =
   36.15    Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   36.16 -  (Method.SIMPLE_METHOD' o tac o local_simpset_of) ;
   36.17 +  (SIMPLE_METHOD' o tac o local_simpset_of) ;
   36.18  
   36.19  (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
   36.20  
   36.21 @@ -419,7 +419,7 @@
   36.22    Method.sectioned_args 
   36.23     (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
   36.24     (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   36.25 -   (fn _ => Method.SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
   36.26 +   (fn _ => SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
   36.27  
   36.28  val perm_simp_meth_debug        = local_simp_meth_setup dperm_simp_tac;
   36.29  val perm_extend_simp_meth       = local_simp_meth_setup perm_extend_simp_tac;
    37.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 13 19:53:09 2009 +0100
    37.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 13 19:58:26 2009 +0100
    37.3 @@ -378,7 +378,7 @@
    37.4             |> snd
    37.5           end)
    37.6        [goals] |>
    37.7 -    Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>
    37.8 +    Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
    37.9        rewrite_goals_tac defs_thms THEN
   37.10        compose_tac (false, rule, length rule_prems) 1), Position.none)) |>
   37.11      Seq.hd
    38.1 --- a/src/HOL/Orderings.thy	Fri Mar 13 19:53:09 2009 +0100
    38.2 +++ b/src/HOL/Orderings.thy	Fri Mar 13 19:58:26 2009 +0100
    38.3 @@ -398,7 +398,7 @@
    38.4  
    38.5  val setup =
    38.6    Method.add_methods
    38.7 -    [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
    38.8 +    [("order", Method.ctxt_args (SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
    38.9    Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
   38.10  
   38.11  end;
    39.1 --- a/src/HOL/Presburger.thy	Fri Mar 13 19:53:09 2009 +0100
    39.2 +++ b/src/HOL/Presburger.thy	Fri Mar 13 19:58:26 2009 +0100
    39.3 @@ -460,7 +460,7 @@
    39.4      (Scan.optional (keyword addN |-- thms) []) -- 
    39.5      (Scan.optional (keyword delN |-- thms) [])) src 
    39.6    #> (fn (((elim, add_ths), del_ths),ctxt) => 
    39.7 -         Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
    39.8 +         SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
    39.9  end
   39.10  *} "Cooper's algorithm for Presburger arithmetic"
   39.11  
    40.1 --- a/src/HOL/Prolog/HOHH.thy	Fri Mar 13 19:53:09 2009 +0100
    40.2 +++ b/src/HOL/Prolog/HOHH.thy	Fri Mar 13 19:58:26 2009 +0100
    40.3 @@ -11,11 +11,11 @@
    40.4  begin
    40.5  
    40.6  method_setup ptac =
    40.7 -  {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
    40.8 +  {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
    40.9    "Basic Lambda Prolog interpreter"
   40.10  
   40.11  method_setup prolog =
   40.12 -  {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
   40.13 +  {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
   40.14    "Lambda Prolog interpreter"
   40.15  
   40.16  consts
    41.1 --- a/src/HOL/SAT.thy	Fri Mar 13 19:53:09 2009 +0100
    41.2 +++ b/src/HOL/SAT.thy	Fri Mar 13 19:58:26 2009 +0100
    41.3 @@ -28,10 +28,10 @@
    41.4  
    41.5  ML {* structure sat = SATFunc(structure cnf = cnf); *}
    41.6  
    41.7 -method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
    41.8 +method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
    41.9    "SAT solver"
   41.10  
   41.11 -method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
   41.12 +method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
   41.13    "SAT solver (with definitional CNF)"
   41.14  
   41.15  end
    42.1 --- a/src/HOL/SET-Protocol/EventSET.thy	Fri Mar 13 19:53:09 2009 +0100
    42.2 +++ b/src/HOL/SET-Protocol/EventSET.thy	Fri Mar 13 19:58:26 2009 +0100
    42.3 @@ -189,7 +189,7 @@
    42.4  *}
    42.5  
    42.6  method_setup analz_mono_contra = {*
    42.7 -    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
    42.8 +    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
    42.9      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   42.10  
   42.11  end
    43.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Fri Mar 13 19:53:09 2009 +0100
    43.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Fri Mar 13 19:58:26 2009 +0100
    43.3 @@ -941,17 +941,17 @@
    43.4  
    43.5  method_setup spy_analz = {*
    43.6      Method.ctxt_args (fn ctxt =>
    43.7 -        Method.SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
    43.8 +        SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
    43.9      "for proving the Fake case when analz is involved"
   43.10  
   43.11  method_setup atomic_spy_analz = {*
   43.12      Method.ctxt_args (fn ctxt =>
   43.13 -        Method.SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
   43.14 +        SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
   43.15      "for debugging spy_analz"
   43.16  
   43.17  method_setup Fake_insert_simp = {*
   43.18      Method.ctxt_args (fn ctxt =>
   43.19 -        Method.SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
   43.20 +        SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
   43.21      "for debugging spy_analz"
   43.22  
   43.23  end
    44.1 --- a/src/HOL/SET-Protocol/PublicSET.thy	Fri Mar 13 19:53:09 2009 +0100
    44.2 +++ b/src/HOL/SET-Protocol/PublicSET.thy	Fri Mar 13 19:58:26 2009 +0100
    44.3 @@ -372,7 +372,7 @@
    44.4  
    44.5  method_setup possibility = {*
    44.6      Method.ctxt_args (fn ctxt =>
    44.7 -        Method.SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
    44.8 +        SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
    44.9      "for proving possibility theorems"
   44.10  
   44.11  
    45.1 --- a/src/HOL/Statespace/state_space.ML	Fri Mar 13 19:53:09 2009 +0100
    45.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Mar 13 19:58:26 2009 +0100
    45.3 @@ -149,7 +149,7 @@
    45.4     thy
    45.5     |> Expression.sublocale_cmd name expr
    45.6     |> Proof.global_terminal_proof
    45.7 -         (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
    45.8 +         (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
    45.9     |> ProofContext.theory_of
   45.10  
   45.11  fun add_locale name expr elems thy =
    46.1 --- a/src/HOL/Tools/function_package/auto_term.ML	Fri Mar 13 19:53:09 2009 +0100
    46.2 +++ b/src/HOL/Tools/function_package/auto_term.ML	Fri Mar 13 19:58:26 2009 +0100
    46.3 @@ -30,7 +30,7 @@
    46.4      THEN PRIMITIVE (inst_thm ctxt rel)
    46.5  
    46.6  val setup = Method.add_methods
    46.7 -  [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
    46.8 +  [("relation", (SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
    46.9      "proves termination using a user-specified wellfounded relation")]
   46.10  
   46.11  end
    47.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Mar 13 19:53:09 2009 +0100
    47.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Mar 13 19:58:26 2009 +0100
    47.3 @@ -155,7 +155,7 @@
    47.4  
    47.5  structure TerminationProver = GenericDataFun
    47.6  (
    47.7 -  type T = (Proof.context -> Method.method)
    47.8 +  type T = Proof.context -> Proof.method
    47.9    val empty = (fn _ => error "Termination prover not configured")
   47.10    val extend = I
   47.11    fun merge _ (a,b) = b (* FIXME *)
    48.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 13 19:53:09 2009 +0100
    48.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 13 19:58:26 2009 +0100
    48.3 @@ -203,7 +203,7 @@
    48.4      handle COMPLETENESS => no_tac)
    48.5  
    48.6  
    48.7 -fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_completeness_tac ctxt)
    48.8 +fun pat_completeness ctxt = SIMPLE_METHOD' (pat_completeness_tac ctxt)
    48.9  
   48.10  val by_pat_completeness_auto =
   48.11      Proof.global_future_terminal_proof
    49.1 --- a/src/HOL/Tools/function_package/induction_scheme.ML	Fri Mar 13 19:53:09 2009 +0100
    49.2 +++ b/src/HOL/Tools/function_package/induction_scheme.ML	Fri Mar 13 19:58:26 2009 +0100
    49.3 @@ -399,7 +399,7 @@
    49.4    mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
    49.5  
    49.6  val setup = Method.add_methods
    49.7 -  [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o induct_scheme_tac),
    49.8 +  [("induct_scheme", Method.ctxt_args (RAW_METHOD o induct_scheme_tac),
    49.9      "proves an induction principle")]
   49.10  
   49.11  end
    50.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Mar 13 19:53:09 2009 +0100
    50.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Mar 13 19:58:26 2009 +0100
    50.3 @@ -218,7 +218,7 @@
    50.4    TRY (FundefCommon.apply_termination_rule ctxt 1)
    50.5    THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))
    50.6  
    50.7 -val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac
    50.8 +val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
    50.9  
   50.10  val setup = Method.add_methods [("lexicographic_order", Method.only_sectioned_args clasimp_modifiers lexicographic_order,
   50.11                                   "termination prover for lexicographic orderings")]
    51.1 --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 13 19:53:09 2009 +0100
    51.2 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 13 19:58:26 2009 +0100
    51.3 @@ -10,7 +10,7 @@
    51.4  
    51.5    val sizechange_tac : Proof.context -> tactic -> tactic
    51.6  
    51.7 -  val decomp_scnp : ScnpSolve.label list -> Proof.context -> method
    51.8 +  val decomp_scnp : ScnpSolve.label list -> Proof.context -> Proof.method
    51.9  
   51.10    val setup : theory -> theory
   51.11  
   51.12 @@ -408,7 +408,7 @@
   51.13      val extra_simps = FundefCommon.TerminationSimps.get ctxt
   51.14      val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
   51.15    in
   51.16 -    Method.SIMPLE_METHOD
   51.17 +    SIMPLE_METHOD
   51.18        (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
   51.19    end
   51.20  
    52.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Mar 13 19:53:09 2009 +0100
    52.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Mar 13 19:58:26 2009 +0100
    52.3 @@ -914,7 +914,7 @@
    52.4  
    52.5  fun arith_method src =
    52.6    Method.syntax Args.bang_facts src
    52.7 -  #> (fn (prems, ctxt) => Method.METHOD (fn facts =>
    52.8 +  #> (fn (prems, ctxt) => METHOD (fn facts =>
    52.9        HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
   52.10        THEN' arith_tac ctxt)));
   52.11  
    53.1 --- a/src/HOL/Tools/metis_tools.ML	Fri Mar 13 19:53:09 2009 +0100
    53.2 +++ b/src/HOL/Tools/metis_tools.ML	Fri Mar 13 19:58:26 2009 +0100
    53.3 @@ -638,7 +638,7 @@
    53.4    val metisH_tac = metis_general_tac ResAtp.Hol;
    53.5  
    53.6    fun method mode = Method.thms_ctxt_args (fn ths => fn ctxt =>
    53.7 -    Method.SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths));
    53.8 +    SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths));
    53.9  
   53.10    val setup =
   53.11      type_lits_setup #>
   53.12 @@ -647,7 +647,7 @@
   53.13         ("metisF", method ResAtp.Fol, "METIS for FOL problems"),
   53.14         ("metisH", method ResAtp.Hol, "METIS for HOL problems"),
   53.15         ("finish_clausify",
   53.16 -         Method.no_args (Method.SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
   53.17 +         Method.no_args (SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
   53.18      "cleanup after conversion to clauses")];
   53.19  
   53.20  end;
    54.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Mar 13 19:53:09 2009 +0100
    54.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Mar 13 19:58:26 2009 +0100
    54.3 @@ -489,7 +489,7 @@
    54.4  
    54.5  val meson_method_setup = Method.add_methods
    54.6    [("meson", Method.thms_args (fn ths =>
    54.7 -      Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
    54.8 +      SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
    54.9      "MESON resolution proof procedure")];
   54.10  
   54.11  
   54.12 @@ -522,7 +522,7 @@
   54.13       end);
   54.14  
   54.15  val setup_methods = Method.add_methods
   54.16 -  [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
   54.17 +  [("neg_clausify", Method.no_args (SIMPLE_METHOD' neg_clausify_tac),
   54.18      "conversion of goal to conjecture clauses")];
   54.19  
   54.20  
    55.1 --- a/src/HOL/Transitive_Closure.thy	Fri Mar 13 19:53:09 2009 +0100
    55.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Mar 13 19:58:26 2009 +0100
    55.3 @@ -695,16 +695,16 @@
    55.4  (* Optional methods *)
    55.5  
    55.6  method_setup trancl =
    55.7 -  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
    55.8 +  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
    55.9    {* simple transitivity reasoner *}
   55.10  method_setup rtrancl =
   55.11 -  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
   55.12 +  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
   55.13    {* simple transitivity reasoner *}
   55.14  method_setup tranclp =
   55.15 -  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
   55.16 +  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
   55.17    {* simple transitivity reasoner (predicate version) *}
   55.18  method_setup rtranclp =
   55.19 -  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
   55.20 +  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
   55.21    {* simple transitivity reasoner (predicate version) *}
   55.22  
   55.23  end
    56.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Fri Mar 13 19:53:09 2009 +0100
    56.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Fri Mar 13 19:58:26 2009 +0100
    56.3 @@ -321,7 +321,7 @@
    56.4  *}
    56.5  
    56.6  method_setup record_auto = {*
    56.7 -  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
    56.8 +  Method.ctxt_args (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
    56.9  *} ""
   56.10  
   56.11  lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
   56.12 @@ -714,7 +714,7 @@
   56.13  
   56.14  method_setup rename_client_map = {*
   56.15    Method.ctxt_args (fn ctxt =>
   56.16 -    Method.SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
   56.17 +    SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
   56.18  *} ""
   56.19  
   56.20  text{*Lifting @{text Client_Increasing} to @{term systemState}*}
    57.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Mar 13 19:53:09 2009 +0100
    57.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Mar 13 19:58:26 2009 +0100
    57.3 @@ -125,7 +125,7 @@
    57.4  
    57.5  method_setup ns_induct = {*
    57.6      Method.ctxt_args (fn ctxt =>
    57.7 -        Method.SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
    57.8 +        SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
    57.9      "for inductive reasoning about the Needham-Schroeder protocol"
   57.10  
   57.11  text{*Converts invariants into statements about reachable states*}
    58.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Fri Mar 13 19:53:09 2009 +0100
    58.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Fri Mar 13 19:58:26 2009 +0100
    58.3 @@ -11,7 +11,7 @@
    58.4  
    58.5  method_setup safety = {*
    58.6      Method.ctxt_args (fn ctxt =>
    58.7 -        Method.SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
    58.8 +        SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
    58.9      "for proving safety properties"
   58.10  
   58.11  method_setup ensures_tac = {*
    59.1 --- a/src/HOL/ex/Binary.thy	Fri Mar 13 19:53:09 2009 +0100
    59.2 +++ b/src/HOL/ex/Binary.thy	Fri Mar 13 19:58:26 2009 +0100
    59.3 @@ -174,7 +174,7 @@
    59.4  simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
    59.5  
    59.6  method_setup binary_simp = {*
    59.7 -  Method.no_args (Method.SIMPLE_METHOD'
    59.8 +  Method.no_args (SIMPLE_METHOD'
    59.9      (full_simp_tac
   59.10        (HOL_basic_ss
   59.11          addsimps @{thms binary_simps}
    60.1 --- a/src/HOL/ex/SAT_Examples.thy	Fri Mar 13 19:53:09 2009 +0100
    60.2 +++ b/src/HOL/ex/SAT_Examples.thy	Fri Mar 13 19:58:26 2009 +0100
    60.3 @@ -83,7 +83,7 @@
    60.4  ML {* reset quick_and_dirty; *}
    60.5  
    60.6  method_setup rawsat =
    60.7 -  {* Method.no_args (Method.SIMPLE_METHOD' sat.rawsat_tac) *}
    60.8 +  {* Method.no_args (SIMPLE_METHOD' sat.rawsat_tac) *}
    60.9    "SAT solver (no preprocessing)"
   60.10  
   60.11  (* ML {* Toplevel.profiling := 1; *} *)
    61.1 --- a/src/Provers/clasimp.ML	Fri Mar 13 19:53:09 2009 +0100
    61.2 +++ b/src/Provers/clasimp.ML	Fri Mar 13 19:58:26 2009 +0100
    61.3 @@ -290,10 +290,10 @@
    61.4  
    61.5  (* methods *)
    61.6  
    61.7 -fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
    61.8 +fun clasimp_meth tac prems ctxt = METHOD (fn facts =>
    61.9    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_clasimpset_of ctxt));
   61.10  
   61.11 -fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
   61.12 +fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
   61.13    HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt)));
   61.14  
   61.15  val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
    62.1 --- a/src/Provers/classical.ML	Fri Mar 13 19:53:09 2009 +0100
    62.2 +++ b/src/Provers/classical.ML	Fri Mar 13 19:58:26 2009 +0100
    62.3 @@ -971,11 +971,8 @@
    62.4  
    62.5  (** proof methods **)
    62.6  
    62.7 -fun METHOD_CLASET tac ctxt =
    62.8 -  Method.METHOD (tac ctxt (local_claset_of ctxt));
    62.9 -
   62.10 -fun METHOD_CLASET' tac ctxt =
   62.11 -  Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
   62.12 +fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt));
   62.13 +fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
   62.14  
   62.15  
   62.16  local
   62.17 @@ -1021,10 +1018,10 @@
   62.18    Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
   62.19    Args.del -- Args.colon >> K (I, rule_del)];
   62.20  
   62.21 -fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   62.22 +fun cla_meth tac prems ctxt = METHOD (fn facts =>
   62.23    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
   62.24  
   62.25 -fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
   62.26 +fun cla_meth' tac prems ctxt = METHOD (fn facts =>
   62.27    HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
   62.28  
   62.29  val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
    63.1 --- a/src/Provers/hypsubst.ML	Fri Mar 13 19:53:09 2009 +0100
    63.2 +++ b/src/Provers/hypsubst.ML	Fri Mar 13 19:58:26 2009 +0100
    63.3 @@ -285,8 +285,8 @@
    63.4  
    63.5  val hypsubst_setup =
    63.6    Method.add_methods
    63.7 -    [("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
    63.8 +    [("hypsubst", Method.no_args (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
    63.9          "substitution using an assumption (improper)"),
   63.10 -     ("simplesubst", Method.thm_args (Method.SIMPLE_METHOD' o stac), "simple substitution")];
   63.11 +     ("simplesubst", Method.thm_args (SIMPLE_METHOD' o stac), "simple substitution")];
   63.12  
   63.13  end;
    64.1 --- a/src/Provers/splitter.ML	Fri Mar 13 19:53:09 2009 +0100
    64.2 +++ b/src/Provers/splitter.ML	Fri Mar 13 19:58:26 2009 +0100
    64.3 @@ -474,7 +474,7 @@
    64.4  
    64.5  fun split_meth src =
    64.6    Method.syntax Attrib.thms src
    64.7 -  #> (fn (ths, _) => Method.SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
    64.8 +  #> (fn (ths, _) => SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
    64.9  
   64.10  
   64.11  (* theory setup *)
    65.1 --- a/src/Pure/Isar/class_target.ML	Fri Mar 13 19:53:09 2009 +0100
    65.2 +++ b/src/Pure/Isar/class_target.ML	Fri Mar 13 19:58:26 2009 +0100
    65.3 @@ -616,9 +616,9 @@
    65.4  
    65.5  val _ = Context.>> (Context.map_theory
    65.6    (Method.add_methods
    65.7 -   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    65.8 +   [("intro_classes", Method.no_args (METHOD intro_classes_tac),
    65.9        "back-chain introduction rules of classes"),
   65.10 -    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   65.11 +    ("default", Method.thms_ctxt_args (METHOD oo default_tac),
   65.12        "apply some intro/elim rule")]));
   65.13  
   65.14  end;
    66.1 --- a/src/Pure/Isar/element.ML	Fri Mar 13 19:53:09 2009 +0100
    66.2 +++ b/src/Pure/Isar/element.ML	Fri Mar 13 19:58:26 2009 +0100
    66.3 @@ -268,7 +268,7 @@
    66.4  local
    66.5  
    66.6  val refine_witness =
    66.7 -  Proof.refine (Method.Basic (K (Method.RAW_METHOD
    66.8 +  Proof.refine (Method.Basic (K (RAW_METHOD
    66.9      (K (ALLGOALS
   66.10        (CONJUNCTS (ALLGOALS
   66.11          (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
    67.1 --- a/src/Pure/Isar/locale.ML	Fri Mar 13 19:53:09 2009 +0100
    67.2 +++ b/src/Pure/Isar/locale.ML	Fri Mar 13 19:58:26 2009 +0100
    67.3 @@ -489,10 +489,10 @@
    67.4  val _ = Context.>> (Context.map_theory
    67.5    (Method.add_methods
    67.6      [("intro_locales",
    67.7 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
    67.8 +      Method.ctxt_args (fn ctxt => METHOD (intro_locales_tac false ctxt)),
    67.9        "back-chain introduction rules of locales without unfolding predicates"),
   67.10       ("unfold_locales",
   67.11 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
   67.12 +      Method.ctxt_args (fn ctxt => METHOD (intro_locales_tac true ctxt)),
   67.13        "back-chain all introduction rules of locales")]));
   67.14  
   67.15  end;
    68.1 --- a/src/Pure/Isar/proof.ML	Fri Mar 13 19:53:09 2009 +0100
    68.2 +++ b/src/Pure/Isar/proof.ML	Fri Mar 13 19:58:26 2009 +0100
    68.3 @@ -780,7 +780,7 @@
    68.4    in (rev vars, props') end;
    68.5  
    68.6  fun refine_terms n =
    68.7 -  refine (Method.Basic (K (Method.RAW_METHOD
    68.8 +  refine (Method.Basic (K (RAW_METHOD
    68.9      (K (HEADGOAL (PRECISE_CONJUNCTS n
   68.10        (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none))
   68.11    #> Seq.hd;
    69.1 --- a/src/Pure/Isar/rule_insts.ML	Fri Mar 13 19:53:09 2009 +0100
    69.2 +++ b/src/Pure/Isar/rule_insts.ML	Fri Mar 13 19:58:26 2009 +0100
    69.3 @@ -387,9 +387,9 @@
    69.4  local
    69.5  
    69.6  fun gen_inst _ tac _ (quant, ([], thms)) =
    69.7 -      Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
    69.8 +      METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
    69.9    | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
   69.10 -      Method.METHOD (fn facts =>
   69.11 +      METHOD (fn facts =>
   69.12          quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm))
   69.13    | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
   69.14  
    70.1 --- a/src/Pure/simplifier.ML	Fri Mar 13 19:53:09 2009 +0100
    70.2 +++ b/src/Pure/simplifier.ML	Fri Mar 13 19:58:26 2009 +0100
    70.3 @@ -410,11 +410,11 @@
    70.4    Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options)
    70.5      (more_mods @ simp_modifiers');
    70.6  
    70.7 -fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
    70.8 +fun simp_method (prems, tac) ctxt = METHOD (fn facts =>
    70.9    ALLGOALS (Method.insert_tac (prems @ facts)) THEN
   70.10      (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
   70.11  
   70.12 -fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
   70.13 +fun simp_method' (prems, tac) ctxt = METHOD (fn facts =>
   70.14    HEADGOAL (Method.insert_tac (prems @ facts) THEN'
   70.15        ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
   70.16  
    71.1 --- a/src/Sequents/ILL.thy	Fri Mar 13 19:53:09 2009 +0100
    71.2 +++ b/src/Sequents/ILL.thy	Fri Mar 13 19:58:26 2009 +0100
    71.3 @@ -146,7 +146,7 @@
    71.4  *}
    71.5  
    71.6  method_setup best_lazy =
    71.7 -  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *}
    71.8 +  {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
    71.9    "lazy classical reasoning"
   71.10  
   71.11  lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
   71.12 @@ -282,10 +282,10 @@
   71.13  
   71.14  
   71.15  method_setup best_safe =
   71.16 -  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} ""
   71.17 +  {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
   71.18  
   71.19  method_setup best_power =
   71.20 -  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} ""
   71.21 +  {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
   71.22  
   71.23  
   71.24  (* Some examples from Troelstra and van Dalen *)
    72.1 --- a/src/Sequents/LK0.thy	Fri Mar 13 19:53:09 2009 +0100
    72.2 +++ b/src/Sequents/LK0.thy	Fri Mar 13 19:58:26 2009 +0100
    72.3 @@ -240,23 +240,23 @@
    72.4  *}
    72.5  
    72.6  method_setup fast_prop =
    72.7 -  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac prop_pack)) *}
    72.8 +  {* Method.no_args (SIMPLE_METHOD' (fast_tac prop_pack)) *}
    72.9    "propositional reasoning"
   72.10  
   72.11  method_setup fast =
   72.12 -  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_pack)) *}
   72.13 +  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_pack)) *}
   72.14    "classical reasoning"
   72.15  
   72.16  method_setup fast_dup =
   72.17 -  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
   72.18 +  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
   72.19    "classical reasoning"
   72.20  
   72.21  method_setup best =
   72.22 -  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_pack)) *}
   72.23 +  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_pack)) *}
   72.24    "classical reasoning"
   72.25  
   72.26  method_setup best_dup =
   72.27 -  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
   72.28 +  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
   72.29    "classical reasoning"
   72.30  
   72.31  
    73.1 --- a/src/Sequents/S4.thy	Fri Mar 13 19:53:09 2009 +0100
    73.2 +++ b/src/Sequents/S4.thy	Fri Mar 13 19:58:26 2009 +0100
    73.3 @@ -45,7 +45,7 @@
    73.4  *}
    73.5  
    73.6  method_setup S4_solve =
    73.7 -  {* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
    73.8 +  {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
    73.9  
   73.10  
   73.11  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    74.1 --- a/src/Sequents/S43.thy	Fri Mar 13 19:53:09 2009 +0100
    74.2 +++ b/src/Sequents/S43.thy	Fri Mar 13 19:58:26 2009 +0100
    74.3 @@ -92,7 +92,7 @@
    74.4  
    74.5  
    74.6  method_setup S43_solve = {*
    74.7 -  Method.no_args (Method.SIMPLE_METHOD
    74.8 +  Method.no_args (SIMPLE_METHOD
    74.9      (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))
   74.10  *} "S4 solver"
   74.11  
    75.1 --- a/src/Sequents/T.thy	Fri Mar 13 19:53:09 2009 +0100
    75.2 +++ b/src/Sequents/T.thy	Fri Mar 13 19:58:26 2009 +0100
    75.3 @@ -44,7 +44,7 @@
    75.4  *}
    75.5  
    75.6  method_setup T_solve =
    75.7 -  {* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
    75.8 +  {* Method.no_args (SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
    75.9  
   75.10  
   75.11  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    76.1 --- a/src/Tools/atomize_elim.ML	Fri Mar 13 19:53:09 2009 +0100
    76.2 +++ b/src/Tools/atomize_elim.ML	Fri Mar 13 19:58:26 2009 +0100
    76.3 @@ -132,7 +132,7 @@
    76.4      end)
    76.5  
    76.6  val setup = Method.add_methods
    76.7 -  [("atomize_elim", Method.ctxt_args (Method.SIMPLE_METHOD' o atomize_elim_tac),
    76.8 +  [("atomize_elim", Method.ctxt_args (SIMPLE_METHOD' o atomize_elim_tac),
    76.9      "convert obtains statement to atomic object logic goal")]
   76.10    #> AtomizeElimData.setup
   76.11  
    77.1 --- a/src/Tools/coherent.ML	Fri Mar 13 19:53:09 2009 +0100
    77.2 +++ b/src/Tools/coherent.ML	Fri Mar 13 19:58:26 2009 +0100
    77.3 @@ -225,7 +225,7 @@
    77.4      end) context 1) ctxt;
    77.5  
    77.6  fun coherent_meth rules ctxt =
    77.7 -  Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
    77.8 +  METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
    77.9  
   77.10  val setup = Method.add_method
   77.11    ("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula");
    78.1 --- a/src/Tools/eqsubst.ML	Fri Mar 13 19:53:09 2009 +0100
    78.2 +++ b/src/Tools/eqsubst.ML	Fri Mar 13 19:58:26 2009 +0100
    78.3 @@ -434,7 +434,7 @@
    78.4  (* inthms are the given arguments in Isar, and treated as eqstep with
    78.5     the first one, then the second etc *)
    78.6  fun eqsubst_meth ctxt occL inthms =
    78.7 -    Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
    78.8 +    SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
    78.9  
   78.10  (* apply a substitution inside assumption j, keeps asm in the same place *)
   78.11  fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
   78.12 @@ -548,7 +548,7 @@
   78.13  (* inthms are the given arguments in Isar, and treated as eqstep with
   78.14     the first one, then the second etc *)
   78.15  fun eqsubst_asm_meth ctxt occL inthms =
   78.16 -    Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
   78.17 +    SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
   78.18  
   78.19  (* syntax for options, given "(asm)" will give back true, without
   78.20     gives back false *)
    79.1 --- a/src/Tools/induct.ML	Fri Mar 13 19:53:09 2009 +0100
    79.2 +++ b/src/Tools/induct.ML	Fri Mar 13 19:58:26 2009 +0100
    79.3 @@ -738,20 +738,20 @@
    79.4  fun cases_meth src =
    79.5    Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
    79.6    #> (fn ((insts, opt_rule), ctxt) =>
    79.7 -    Method.METHOD_CASES (fn facts =>
    79.8 +    METHOD_CASES (fn facts =>
    79.9        Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
   79.10  
   79.11  fun induct_meth src =
   79.12    Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   79.13      (arbitrary -- taking -- Scan.option induct_rule)) src
   79.14    #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
   79.15 -    Method.RAW_METHOD_CASES (fn facts =>
   79.16 +    RAW_METHOD_CASES (fn facts =>
   79.17        Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
   79.18  
   79.19  fun coinduct_meth src =
   79.20    Method.syntax (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule) src
   79.21    #> (fn (((insts, taking), opt_rule), ctxt) =>
   79.22 -    Method.RAW_METHOD_CASES (fn facts =>
   79.23 +    RAW_METHOD_CASES (fn facts =>
   79.24        Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
   79.25  
   79.26  end;
    80.1 --- a/src/Tools/intuitionistic.ML	Fri Mar 13 19:53:09 2009 +0100
    80.2 +++ b/src/Tools/intuitionistic.ML	Fri Mar 13 19:58:26 2009 +0100
    80.3 @@ -86,7 +86,7 @@
    80.4  
    80.5  val method =
    80.6    Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
    80.7 -    (fn n => fn prems => fn ctxt => Method.METHOD (fn facts =>
    80.8 +    (fn n => fn prems => fn ctxt => METHOD (fn facts =>
    80.9        HEADGOAL (Method.insert_tac (prems @ facts) THEN'
   80.10        ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
   80.11  
    81.1 --- a/src/ZF/Tools/typechk.ML	Fri Mar 13 19:53:09 2009 +0100
    81.2 +++ b/src/ZF/Tools/typechk.ML	Fri Mar 13 19:58:26 2009 +0100
    81.3 @@ -116,7 +116,7 @@
    81.4    Method.only_sectioned_args
    81.5      [Args.add -- Args.colon >> K (I, TC_add),
    81.6       Args.del -- Args.colon >> K (I, TC_del)]
    81.7 -  (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
    81.8 +  (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
    81.9  
   81.10  val _ =
   81.11    OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
    82.1 --- a/src/ZF/UNITY/Constrains.thy	Fri Mar 13 19:53:09 2009 +0100
    82.2 +++ b/src/ZF/UNITY/Constrains.thy	Fri Mar 13 19:58:26 2009 +0100
    82.3 @@ -496,13 +496,11 @@
    82.4  setup ProgramDefs.setup
    82.5  
    82.6  method_setup safety = {*
    82.7 -  Method.ctxt_args (fn ctxt =>
    82.8 -    Method.SIMPLE_METHOD' (constrains_tac ctxt)) *}
    82.9 +  Method.ctxt_args (SIMPLE_METHOD' o constrains_tac) *}
   82.10    "for proving safety properties"
   82.11  
   82.12  method_setup always = {*
   82.13 -  Method.ctxt_args (fn ctxt =>
   82.14 -    Method.SIMPLE_METHOD' (always_tac ctxt)) *}
   82.15 +  Method.ctxt_args (SIMPLE_METHOD' o always_tac) *}
   82.16    "for proving invariants"
   82.17  
   82.18  end