# HG changeset patch
# User wenzelm
# Date 1236970706 -3600
# Node ID 4120fc59dd8591021cc7794619b694d69f44a19b
# Parent  e19d5b459a61542f6d31b90ace5cd13c858a54cc
unified type Proof.method and pervasive METHOD combinators;

diff -r e19d5b459a61 -r 4120fc59dd85 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -895,11 +895,10 @@
 %FIXME proper antiquotations
 {\footnotesize
 \begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
-    Method.METHOD (fn facts => foobar_tac))
+ Method.no_args (METHOD (fn facts => foobar_tac))
+ Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
+ Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac))
 \end{verbatim}
 }
 
diff -r e19d5b459a61 -r 4120fc59dd85 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Fri Mar 13 19:53:09 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Mar 13 19:58:26 2009 +0100
@@ -899,11 +899,10 @@
 %FIXME proper antiquotations
 {\footnotesize
 \begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
-    Method.METHOD (fn facts => foobar_tac))
+ Method.no_args (METHOD (fn facts => foobar_tac))
+ Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
+ Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt => METHOD (fn facts => foobar_tac))
 \end{verbatim}
 }
 
diff -r e19d5b459a61 -r 4120fc59dd85 doc-src/TutorialI/Protocol/Event.thy
--- a/doc-src/TutorialI/Protocol/Event.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Event.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -287,7 +287,7 @@
     intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
 
 method_setup analz_mono_contra = {*
-    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
@@ -344,7 +344,7 @@
 *}
 
 method_setup synth_analz_mono_contra = {*
-    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
+    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
     "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
 (*>*)
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/CCL/Wfd.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -505,7 +505,7 @@
 val eval_setup =
   Data.setup #>
   Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
-    Method.SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")];
+    SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")];
 
 end;
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/Cube/Example.thy
--- a/src/Cube/Example.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Cube/Example.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -15,18 +15,18 @@
 *}
 
 method_setup depth_solve = {*
-  Method.thms_args (fn thms => Method.METHOD (fn facts =>
+  Method.thms_args (fn thms => METHOD (fn facts =>
   (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
 *} ""
 
 method_setup depth_solve1 = {*
-  Method.thms_args (fn thms => Method.METHOD (fn facts =>
+  Method.thms_args (fn thms => METHOD (fn facts =>
   (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
 *} ""
 
 method_setup strip_asms =  {*
   let val strip_b = thm "strip_b" and strip_s = thm "strip_s" in
-    Method.thms_args (fn thms => Method.METHOD (fn facts =>
+    Method.thms_args (fn thms => METHOD (fn facts =>
       REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
   end
 *} ""
diff -r e19d5b459a61 -r 4120fc59dd85 src/FOL/ex/Iff_Oracle.thy
--- a/src/FOL/ex/Iff_Oracle.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/FOL/ex/Iff_Oracle.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -53,7 +53,7 @@
 
 method_setup iff = {*
   Method.simple_args OuterParse.nat (fn n => fn ctxt =>
-    Method.SIMPLE_METHOD
+    SIMPLE_METHOD
       (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
         handle Fail _ => no_tac))
 *} "iff oracle"
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -222,7 +222,7 @@
 *}   (* Note: r_one is not necessary in ring_ss *)
 
 method_setup ring =
-  {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
+  {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
   {* computes distributive normal form in rings *}
 
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -72,7 +72,7 @@
 (** Setup **)
 
 val setup =
-  Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac),
+  Method.add_methods [("algebra", Method.ctxt_args (SIMPLE_METHOD' o algebra_tac),
     "normalisation of algebraic structure")] #>
   Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/Event.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -289,7 +289,7 @@
 *}
 
 method_setup analz_mono_contra = {*
-    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
@@ -310,7 +310,7 @@
 *}
 
 method_setup synth_analz_mono_contra = {*
-    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
+    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
     "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/Message.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -941,18 +941,15 @@
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
 
 method_setup spy_analz = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (Message.gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+    Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
     "for proving the Fake case when analz is involved"
 
 method_setup atomic_spy_analz = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (Message.atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+    Method.ctxt_args (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
     "for debugging spy_analz"
 
 method_setup Fake_insert_simp = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (Message.Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
+    Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
     "for debugging spy_analz"
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Auth/OtwayReesBella.thy
--- a/src/HOL/Auth/OtwayReesBella.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/OtwayReesBella.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -137,7 +137,7 @@
 *}
  
 method_setup parts_explicit = {*
-    Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *}
+    Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *}
   "to explicitly state that some message components belong to parts knows Spy"
 
 
@@ -258,7 +258,7 @@
 
 method_setup analz_freshCryptK = {*
     Method.ctxt_args (fn ctxt =>
-     (Method.SIMPLE_METHOD
+     (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
           ALLGOALS (asm_simp_tac
@@ -268,7 +268,7 @@
 
 method_setup disentangle = {*
     Method.no_args
-     (Method.SIMPLE_METHOD
+     (SIMPLE_METHOD
       (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
                    ORELSE' hyp_subst_tac))) *}
   "for eliminating conjunctions, disjunctions and the like"
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/Public.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -425,7 +425,7 @@
 
 method_setup analz_freshK = {*
     Method.ctxt_args (fn ctxt =>
-     (Method.SIMPLE_METHOD
+     (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *}
@@ -435,13 +435,11 @@
 subsection{*Specialized Methods for Possibility Theorems*}
 
 method_setup possibility = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (Public.possibility_tac ctxt)) *}
+    Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *}
     "for proving possibility theorems"
 
 method_setup basic_possibility = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (Public.basic_possibility_tac ctxt)) *}
+    Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *}
     "for proving possibility theorems"
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/Shared.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -239,20 +239,18 @@
 
 method_setup analz_freshK = {*
     Method.ctxt_args (fn ctxt =>
-     (Method.SIMPLE_METHOD
+     (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (Simplifier.context ctxt Shared.analz_image_freshK_ss))]))) *}
     "for proving the Session Key Compromise theorem"
 
 method_setup possibility = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
+    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
     "for proving possibility theorems"
 
 method_setup basic_possibility = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
+    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
     "for proving possibility theorems"
 
 lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Auth/Smartcard/ShoupRubin.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -769,15 +769,15 @@
 *}
 
 method_setup prepare = {*
-    Method.no_args (Method.SIMPLE_METHOD ShoupRubin.prepare_tac) *}
+    Method.no_args (SIMPLE_METHOD ShoupRubin.prepare_tac) *}
   "to launch a few simple facts that'll help the simplifier"
 
 method_setup parts_prepare = {*
-    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
+    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
   "additional facts to reason about parts"
 
 method_setup analz_prepare = {*
-    Method.no_args (Method.SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
+    Method.no_args (SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
   "additional facts to reason about analz"
 
 
@@ -823,7 +823,7 @@
 
 method_setup sc_analz_freshK = {*
     Method.ctxt_args (fn ctxt =>
-     (Method.SIMPLE_METHOD
+     (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST
        (resolve_tac [allI, ballI, impI]),
         REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Auth/Smartcard/ShoupRubinBella.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -777,15 +777,15 @@
 *}
 
 method_setup prepare = {*
-    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
+    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
   "to launch a few simple facts that'll help the simplifier"
 
 method_setup parts_prepare = {*
-    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
+    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
   "additional facts to reason about parts"
 
 method_setup analz_prepare = {*
-    Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
+    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
   "additional facts to reason about analz"
 
 
@@ -832,7 +832,7 @@
 
 method_setup sc_analz_freshK = {*
     Method.ctxt_args (fn ctxt =>
-     (Method.SIMPLE_METHOD
+     (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -408,7 +408,7 @@
 
 method_setup analz_freshK = {*
     Method.ctxt_args (fn ctxt =>
-     (Method.SIMPLE_METHOD
+     (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss))]))) *}
@@ -416,12 +416,12 @@
 
 method_setup possibility = {*
     Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
+        SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
     "for proving possibility theorems"
 
 method_setup basic_possibility = {*
     Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
+        SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
     "for proving possibility theorems"
 
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Code_Setup.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -226,7 +226,7 @@
 *}
 
 ML {*
-fun gen_eval_method conv = Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD'
+fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD'
   (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
     THEN' rtac TrueI))
 *}
@@ -237,7 +237,7 @@
 method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
   "solve goal by evaluation"
 
-method_setup normalization = {* (Method.no_args o Method.SIMPLE_METHOD')
+method_setup normalization = {* (Method.no_args o SIMPLE_METHOD')
   (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
 *} "solve goal by normalization"
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -2499,7 +2499,7 @@
 method_setup approximation = {* fn src => 
   Method.syntax Args.term src #>
   (fn (prec, ctxt) => let
-   in Method.SIMPLE_METHOD' (fn i =>
+   in SIMPLE_METHOD' (fn i =>
      (DETERM (reify_uneq ctxt i)
       THEN rule_uneq ctxt prec i
       THEN Simplifier.asm_full_simp_tac bounded_by_simpset i 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -295,7 +295,7 @@
 
 use "~~/src/HOL/Tools/Qelim/langford.ML"
 method_setup dlo = {*
-  Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
+  Method.ctxt_args (SIMPLE_METHOD' o LangfordQE.dlo_tac)
 *} "Langford's algorithm for quantifier elimination in dense linear orders"
 
 
@@ -546,7 +546,7 @@
 use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML"
 
 method_setup ferrack = {*
-  Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
+  Method.ctxt_args (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
 *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
 
 subsection {* Ferrante and Rackoff algorithm over ordered fields *}
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -100,7 +100,7 @@
 
 fun linr_meth src =
   Method.syntax (Args.mode "no_quantify") src
-  #> (fn (q, ctxt) => Method.SIMPLE_METHOD' (linr_tac ctxt (not q)));
+  #> (fn (q, ctxt) => SIMPLE_METHOD' (linr_tac ctxt (not q)));
 
 val setup =
   Method.add_method ("rferrack", linr_meth,
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -253,7 +253,7 @@
 
 
 method_setup sring_norm = {*
-  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
+  Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
 *} "semiring normalizer"
 
 
@@ -431,7 +431,7 @@
     ((Scan.optional (keyword addN |-- thms) []) -- 
     (Scan.optional (keyword delN |-- thms) [])) src 
  #> (fn ((add_ths, del_ths), ctxt) => 
-       Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
+       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
 end
 *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
 declare dvd_def[algebra]
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -234,12 +234,12 @@
 use "hoare_tac.ML"
 
 method_setup vcg = {*
-  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+  Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
   "verification condition generator"
 
 method_setup vcg_simp = {*
   Method.ctxt_args (fn ctxt =>
-    Method.SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
+    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   "verification condition generator plus simplification"
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -246,12 +246,12 @@
 use "hoare_tac.ML"
 
 method_setup vcg = {*
-  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+  Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
   "verification condition generator"
 
 method_setup vcg_simp = {*
   Method.ctxt_args (fn ctxt =>
-    Method.SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
+    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   "verification condition generator plus simplification"
 
 (* Special syntax for guarded statements and guarded array updates: *)
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/HoareParallel/OG_Tactics.thy
--- a/src/HOL/HoareParallel/OG_Tactics.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/HoareParallel/OG_Tactics.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -465,21 +465,21 @@
 Isabelle proofs. *}
 
 method_setup oghoare = {*
-  Method.no_args (Method.SIMPLE_METHOD' oghoare_tac) *}
+  Method.no_args (SIMPLE_METHOD' oghoare_tac) *}
   "verification condition generator for the oghoare logic"
 
 method_setup annhoare = {*
-  Method.no_args (Method.SIMPLE_METHOD' annhoare_tac) *}
+  Method.no_args (SIMPLE_METHOD' annhoare_tac) *}
   "verification condition generator for the ann_hoare logic"
 
 method_setup interfree_aux = {*
-  Method.no_args (Method.SIMPLE_METHOD' interfree_aux_tac) *}
+  Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *}
   "verification condition generator for interference freedom tests"
 
 text {* Tactics useful for dealing with the generated verification conditions: *}
 
 method_setup conjI_tac = {*
-  Method.no_args (Method.SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
+  Method.no_args (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
   "verification condition generator for interference freedom tests"
 
 ML {*
@@ -490,7 +490,7 @@
 *}
 
 method_setup disjE_tac = {*
-  Method.no_args (Method.SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
+  Method.no_args (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
   "verification condition generator for interference freedom tests"
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Import/import_package.ML
--- a/src/HOL/Import/import_package.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Import/import_package.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -73,7 +73,7 @@
                       let
                           val thy = ProofContext.theory_of ctxt
                       in
-                          Method.SIMPLE_METHOD (import_tac arg thy)
+                          SIMPLE_METHOD (import_tac arg thy)
                       end)
 
 val setup = Method.add_method("import",import_meth,"Import HOL4 theorem")
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Import/shuffler.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -656,7 +656,7 @@
     let
         val thy = ProofContext.theory_of ctxt
     in
-        Method.SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
+        SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
     end
 
 fun search_meth ctxt =
@@ -664,7 +664,7 @@
         val thy = ProofContext.theory_of ctxt
         val prems = Assumption.all_prems_of ctxt
     in
-        Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
+        SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
     end
 
 fun add_shuffle_rule thm thy =
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -455,7 +455,7 @@
 
 method_setup hoare = {*
   Method.ctxt_args (fn ctxt =>
-    (Method.SIMPLE_METHOD'
+    (SIMPLE_METHOD'
        (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}
   "verification condition generator for Hoare logic"
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -134,7 +134,7 @@
    (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
    THEN' asm_full_simp_tac (ss2 addsimps ths)
  in
-  Method.thms_args (Method.SIMPLE_METHOD' o vector_arith_tac)
+  Method.thms_args (SIMPLE_METHOD' o vector_arith_tac)
 end
 *} "Lifts trivial vector statements to real arith statements"
 
@@ -948,7 +948,7 @@
 
 use "normarith.ML"
 
-method_setup norm = {* Method.ctxt_args (Method.SIMPLE_METHOD' o NormArith.norm_arith_tac)
+method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
 *} "Proves simple linear statements about vector norms"
 
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -84,7 +84,7 @@
 
 in
   Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
-    Method.SIMPLE_METHOD' (eval_tac ws))
+    SIMPLE_METHOD' (eval_tac ws))
 end
 *} "Evaluation with ML witnesses"
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Library/Reflection.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -19,7 +19,7 @@
 method_setup reify = {* fn src =>
   Method.syntax (Attrib.thms --
     Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
-  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
+  (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
 *} "partial automatic reification"
 
 method_setup reflection = {* 
@@ -38,7 +38,7 @@
         val (ceqs,cths) = Reify_Data.get ctxt 
         val corr_thms = ths@cths
         val raw_eqs = eqs@ceqs
-      in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
+      in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
      end) end
 *} "reflection method"
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -978,7 +978,7 @@
   val ss1 = HOL_basic_ss addsimps [@{thm expand_fun_eq} RS sym]
   val ss2 = HOL_basic_ss addsimps [@{thm mknet_inverse'}]
   fun tac ths = ObjectLogic.full_atomize_tac THEN' Simplifier.simp_tac (ss1 addsimps ths) THEN' Simplifier.asm_full_simp_tac ss2
-  in Method.thms_args (Method.SIMPLE_METHOD' o tac) end
+  in Method.thms_args (SIMPLE_METHOD' o tac) end
 
 *} "Reduces goals about net"
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Library/comm_ring.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -101,7 +101,7 @@
   end);
 
 val comm_ring_meth =
-  Method.ctxt_args (Method.SIMPLE_METHOD' o comm_ring_tac);
+  Method.ctxt_args (SIMPLE_METHOD' o comm_ring_tac);
 
 val setup =
   Method.add_method ("comm_ring", comm_ring_meth,
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/NSA/transfer.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -116,6 +116,6 @@
      ("transfer_refold", Attrib.add_del_args refold_add refold_del,
       "declaration of transfer refolding rule")] #>
   Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt =>
-    Method.SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
+    SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
 
 end;
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -204,4 +204,4 @@
 
 val setup_fresh_fun_simp =
   Method.simple_args options_syntax 
-  (fn b => fn _ => Method.SIMPLE_METHOD (fresh_fun_tac b 1))
+  (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1))
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -8,7 +8,7 @@
   val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     (string * typ) list -> (string * typ) list list -> thm list ->
     thm list -> int -> RuleCases.cases_tactic
-  val nominal_induct_method: Method.src -> Proof.context -> Method.method
+  val nominal_induct_method: Method.src -> Proof.context -> Proof.method
 end =
 struct
 
@@ -157,7 +157,7 @@
    (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
     avoiding -- fixing -- rule_spec) src
   #> (fn ((((x, y), z), w), ctxt) =>
-    Method.RAW_METHOD_CASES (fn facts =>
+    RAW_METHOD_CASES (fn facts =>
       HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
 
 end;
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -400,7 +400,7 @@
   Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) ||
   Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
 
-fun perm_simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
+fun perm_simp_method (prems, tac) ctxt = METHOD (fn facts =>
    HEADGOAL (Method.insert_tac (prems @ facts) THEN'
        ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
 
@@ -411,7 +411,7 @@
 (* setup so that the simpset is used which is active at the moment when the tactic is called *)
 fun local_simp_meth_setup tac =
   Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
-  (Method.SIMPLE_METHOD' o tac o local_simpset_of) ;
+  (SIMPLE_METHOD' o tac o local_simpset_of) ;
 
 (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
 
@@ -419,7 +419,7 @@
   Method.sectioned_args 
    (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
    (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
-   (fn _ => Method.SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
+   (fn _ => SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
 
 val perm_simp_meth_debug        = local_simp_meth_setup dperm_simp_tac;
 val perm_extend_simp_meth       = local_simp_meth_setup perm_extend_simp_tac;
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -378,7 +378,7 @@
            |> snd
          end)
       [goals] |>
-    Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>
+    Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
       rewrite_goals_tac defs_thms THEN
       compose_tac (false, rule, length rule_prems) 1), Position.none)) |>
     Seq.hd
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Orderings.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -398,7 +398,7 @@
 
 val setup =
   Method.add_methods
-    [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
+    [("order", Method.ctxt_args (SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
   Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
 
 end;
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Presburger.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -460,7 +460,7 @@
     (Scan.optional (keyword addN |-- thms) []) -- 
     (Scan.optional (keyword delN |-- thms) [])) src 
   #> (fn (((elim, add_ths), del_ths),ctxt) => 
-         Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
+         SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
 end
 *} "Cooper's algorithm for Presburger arithmetic"
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Prolog/HOHH.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -11,11 +11,11 @@
 begin
 
 method_setup ptac =
-  {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
+  {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
   "Basic Lambda Prolog interpreter"
 
 method_setup prolog =
-  {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
+  {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
   "Lambda Prolog interpreter"
 
 consts
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/SAT.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -28,10 +28,10 @@
 
 ML {* structure sat = SATFunc(structure cnf = cnf); *}
 
-method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
+method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
   "SAT solver"
 
-method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
+method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
   "SAT solver (with definitional CNF)"
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/SET-Protocol/EventSET.thy
--- a/src/HOL/SET-Protocol/EventSET.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/SET-Protocol/EventSET.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -189,7 +189,7 @@
 *}
 
 method_setup analz_mono_contra = {*
-    Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/SET-Protocol/MessageSET.thy
--- a/src/HOL/SET-Protocol/MessageSET.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -941,17 +941,17 @@
 
 method_setup spy_analz = {*
     Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
+        SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
     "for proving the Fake case when analz is involved"
 
 method_setup atomic_spy_analz = {*
     Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
+        SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
     "for debugging spy_analz"
 
 method_setup Fake_insert_simp = {*
     Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
+        SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
     "for debugging spy_analz"
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/SET-Protocol/PublicSET.thy
--- a/src/HOL/SET-Protocol/PublicSET.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/SET-Protocol/PublicSET.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -372,7 +372,7 @@
 
 method_setup possibility = {*
     Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
+        SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
     "for proving possibility theorems"
 
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -149,7 +149,7 @@
    thy
    |> Expression.sublocale_cmd name expr
    |> Proof.global_terminal_proof
-         (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
+         (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
    |> ProofContext.theory_of
 
 fun add_locale name expr elems thy =
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Tools/function_package/auto_term.ML
--- a/src/HOL/Tools/function_package/auto_term.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/function_package/auto_term.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -30,7 +30,7 @@
     THEN PRIMITIVE (inst_thm ctxt rel)
 
 val setup = Method.add_methods
-  [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
+  [("relation", (SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
     "proves termination using a user-specified wellfounded relation")]
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -155,7 +155,7 @@
 
 structure TerminationProver = GenericDataFun
 (
-  type T = (Proof.context -> Method.method)
+  type T = Proof.context -> Proof.method
   val empty = (fn _ => error "Termination prover not configured")
   val extend = I
   fun merge _ (a,b) = b (* FIXME *)
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -203,7 +203,7 @@
     handle COMPLETENESS => no_tac)
 
 
-fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_completeness_tac ctxt)
+fun pat_completeness ctxt = SIMPLE_METHOD' (pat_completeness_tac ctxt)
 
 val by_pat_completeness_auto =
     Proof.global_future_terminal_proof
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Tools/function_package/induction_scheme.ML
--- a/src/HOL/Tools/function_package/induction_scheme.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/function_package/induction_scheme.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -399,7 +399,7 @@
   mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
 
 val setup = Method.add_methods
-  [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o induct_scheme_tac),
+  [("induct_scheme", Method.ctxt_args (RAW_METHOD o induct_scheme_tac),
     "proves an induction principle")]
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -218,7 +218,7 @@
   TRY (FundefCommon.apply_termination_rule ctxt 1)
   THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))
 
-val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac
+val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
 
 val setup = Method.add_methods [("lexicographic_order", Method.only_sectioned_args clasimp_modifiers lexicographic_order,
                                  "termination prover for lexicographic orderings")]
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Tools/function_package/scnp_reconstruct.ML
--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -10,7 +10,7 @@
 
   val sizechange_tac : Proof.context -> tactic -> tactic
 
-  val decomp_scnp : ScnpSolve.label list -> Proof.context -> method
+  val decomp_scnp : ScnpSolve.label list -> Proof.context -> Proof.method
 
   val setup : theory -> theory
 
@@ -408,7 +408,7 @@
     val extra_simps = FundefCommon.TerminationSimps.get ctxt
     val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
   in
-    Method.SIMPLE_METHOD
+    SIMPLE_METHOD
       (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
   end
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -914,7 +914,7 @@
 
 fun arith_method src =
   Method.syntax Args.bang_facts src
-  #> (fn (prems, ctxt) => Method.METHOD (fn facts =>
+  #> (fn (prems, ctxt) => METHOD (fn facts =>
       HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
       THEN' arith_tac ctxt)));
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -638,7 +638,7 @@
   val metisH_tac = metis_general_tac ResAtp.Hol;
 
   fun method mode = Method.thms_ctxt_args (fn ths => fn ctxt =>
-    Method.SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths));
+    SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths));
 
   val setup =
     type_lits_setup #>
@@ -647,7 +647,7 @@
        ("metisF", method ResAtp.Fol, "METIS for FOL problems"),
        ("metisH", method ResAtp.Hol, "METIS for HOL problems"),
        ("finish_clausify",
-         Method.no_args (Method.SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
+         Method.no_args (SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
     "cleanup after conversion to clauses")];
 
 end;
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -489,7 +489,7 @@
 
 val meson_method_setup = Method.add_methods
   [("meson", Method.thms_args (fn ths =>
-      Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
+      SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
     "MESON resolution proof procedure")];
 
 
@@ -522,7 +522,7 @@
      end);
 
 val setup_methods = Method.add_methods
-  [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
+  [("neg_clausify", Method.no_args (SIMPLE_METHOD' neg_clausify_tac),
     "conversion of goal to conjecture clauses")];
 
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -695,16 +695,16 @@
 (* Optional methods *)
 
 method_setup trancl =
-  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
+  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
   {* simple transitivity reasoner *}
 method_setup rtrancl =
-  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
+  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
   {* simple transitivity reasoner *}
 method_setup tranclp =
-  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
+  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
   {* simple transitivity reasoner (predicate version) *}
 method_setup rtranclp =
-  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
+  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
   {* simple transitivity reasoner (predicate version) *}
 
 end
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -321,7 +321,7 @@
 *}
 
 method_setup record_auto = {*
-  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
+  Method.ctxt_args (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
 *} ""
 
 lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
@@ -714,7 +714,7 @@
 
 method_setup rename_client_map = {*
   Method.ctxt_args (fn ctxt =>
-    Method.SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
+    SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
 *} ""
 
 text{*Lifting @{text Client_Increasing} to @{term systemState}*}
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/UNITY/Simple/NSP_Bad.thy
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -125,7 +125,7 @@
 
 method_setup ns_induct = {*
     Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
+        SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
     "for inductive reasoning about the Needham-Schroeder protocol"
 
 text{*Converts invariants into statements about reachable states*}
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -11,7 +11,7 @@
 
 method_setup safety = {*
     Method.ctxt_args (fn ctxt =>
-        Method.SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
+        SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
     "for proving safety properties"
 
 method_setup ensures_tac = {*
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/ex/Binary.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -174,7 +174,7 @@
 simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
 
 method_setup binary_simp = {*
-  Method.no_args (Method.SIMPLE_METHOD'
+  Method.no_args (SIMPLE_METHOD'
     (full_simp_tac
       (HOL_basic_ss
         addsimps @{thms binary_simps}
diff -r e19d5b459a61 -r 4120fc59dd85 src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/ex/SAT_Examples.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -83,7 +83,7 @@
 ML {* reset quick_and_dirty; *}
 
 method_setup rawsat =
-  {* Method.no_args (Method.SIMPLE_METHOD' sat.rawsat_tac) *}
+  {* Method.no_args (SIMPLE_METHOD' sat.rawsat_tac) *}
   "SAT solver (no preprocessing)"
 
 (* ML {* Toplevel.profiling := 1; *} *)
diff -r e19d5b459a61 -r 4120fc59dd85 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Provers/clasimp.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -290,10 +290,10 @@
 
 (* methods *)
 
-fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
+fun clasimp_meth tac prems ctxt = METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_clasimpset_of ctxt));
 
-fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
+fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt)));
 
 val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
diff -r e19d5b459a61 -r 4120fc59dd85 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Provers/classical.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -971,11 +971,8 @@
 
 (** proof methods **)
 
-fun METHOD_CLASET tac ctxt =
-  Method.METHOD (tac ctxt (local_claset_of ctxt));
-
-fun METHOD_CLASET' tac ctxt =
-  Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
+fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt));
+fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
 
 
 local
@@ -1021,10 +1018,10 @@
   Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
   Args.del -- Args.colon >> K (I, rule_del)];
 
-fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
+fun cla_meth tac prems ctxt = METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
 
-fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
+fun cla_meth' tac prems ctxt = METHOD (fn facts =>
   HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
 
 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
diff -r e19d5b459a61 -r 4120fc59dd85 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Provers/hypsubst.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -285,8 +285,8 @@
 
 val hypsubst_setup =
   Method.add_methods
-    [("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
+    [("hypsubst", Method.no_args (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
         "substitution using an assumption (improper)"),
-     ("simplesubst", Method.thm_args (Method.SIMPLE_METHOD' o stac), "simple substitution")];
+     ("simplesubst", Method.thm_args (SIMPLE_METHOD' o stac), "simple substitution")];
 
 end;
diff -r e19d5b459a61 -r 4120fc59dd85 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Provers/splitter.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -474,7 +474,7 @@
 
 fun split_meth src =
   Method.syntax Attrib.thms src
-  #> (fn (ths, _) => Method.SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
+  #> (fn (ths, _) => SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
 
 
 (* theory setup *)
diff -r e19d5b459a61 -r 4120fc59dd85 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -616,9 +616,9 @@
 
 val _ = Context.>> (Context.map_theory
   (Method.add_methods
-   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
+   [("intro_classes", Method.no_args (METHOD intro_classes_tac),
       "back-chain introduction rules of classes"),
-    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
+    ("default", Method.thms_ctxt_args (METHOD oo default_tac),
       "apply some intro/elim rule")]));
 
 end;
diff -r e19d5b459a61 -r 4120fc59dd85 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Pure/Isar/element.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -268,7 +268,7 @@
 local
 
 val refine_witness =
-  Proof.refine (Method.Basic (K (Method.RAW_METHOD
+  Proof.refine (Method.Basic (K (RAW_METHOD
     (K (ALLGOALS
       (CONJUNCTS (ALLGOALS
         (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
diff -r e19d5b459a61 -r 4120fc59dd85 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -489,10 +489,10 @@
 val _ = Context.>> (Context.map_theory
   (Method.add_methods
     [("intro_locales",
-      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
+      Method.ctxt_args (fn ctxt => METHOD (intro_locales_tac false ctxt)),
       "back-chain introduction rules of locales without unfolding predicates"),
      ("unfold_locales",
-      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
+      Method.ctxt_args (fn ctxt => METHOD (intro_locales_tac true ctxt)),
       "back-chain all introduction rules of locales")]));
 
 end;
diff -r e19d5b459a61 -r 4120fc59dd85 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -780,7 +780,7 @@
   in (rev vars, props') end;
 
 fun refine_terms n =
-  refine (Method.Basic (K (Method.RAW_METHOD
+  refine (Method.Basic (K (RAW_METHOD
     (K (HEADGOAL (PRECISE_CONJUNCTS n
       (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none))
   #> Seq.hd;
diff -r e19d5b459a61 -r 4120fc59dd85 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -387,9 +387,9 @@
 local
 
 fun gen_inst _ tac _ (quant, ([], thms)) =
-      Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
+      METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
   | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
-      Method.METHOD (fn facts =>
+      METHOD (fn facts =>
         quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm))
   | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Pure/simplifier.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -410,11 +410,11 @@
   Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options)
     (more_mods @ simp_modifiers');
 
-fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
+fun simp_method (prems, tac) ctxt = METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN
     (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
 
-fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
+fun simp_method' (prems, tac) ctxt = METHOD (fn facts =>
   HEADGOAL (Method.insert_tac (prems @ facts) THEN'
       ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Sequents/ILL.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -146,7 +146,7 @@
 *}
 
 method_setup best_lazy =
-  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *}
+  {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
   "lazy classical reasoning"
 
 lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
@@ -282,10 +282,10 @@
 
 
 method_setup best_safe =
-  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} ""
+  {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
 
 method_setup best_power =
-  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} ""
+  {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
 
 
 (* Some examples from Troelstra and van Dalen *)
diff -r e19d5b459a61 -r 4120fc59dd85 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Sequents/LK0.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -240,23 +240,23 @@
 *}
 
 method_setup fast_prop =
-  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac prop_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (fast_tac prop_pack)) *}
   "propositional reasoning"
 
 method_setup fast =
-  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_pack)) *}
   "classical reasoning"
 
 method_setup fast_dup =
-  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
   "classical reasoning"
 
 method_setup best =
-  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_pack)) *}
   "classical reasoning"
 
 method_setup best_dup =
-  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
   "classical reasoning"
 
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/Sequents/S4.thy
--- a/src/Sequents/S4.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Sequents/S4.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -45,7 +45,7 @@
 *}
 
 method_setup S4_solve =
-  {* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
+  {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
diff -r e19d5b459a61 -r 4120fc59dd85 src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Sequents/S43.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -92,7 +92,7 @@
 
 
 method_setup S43_solve = {*
-  Method.no_args (Method.SIMPLE_METHOD
+  Method.no_args (SIMPLE_METHOD
     (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))
 *} "S4 solver"
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/Sequents/T.thy
--- a/src/Sequents/T.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Sequents/T.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -44,7 +44,7 @@
 *}
 
 method_setup T_solve =
-  {* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
+  {* Method.no_args (SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
diff -r e19d5b459a61 -r 4120fc59dd85 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Tools/atomize_elim.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -132,7 +132,7 @@
     end)
 
 val setup = Method.add_methods
-  [("atomize_elim", Method.ctxt_args (Method.SIMPLE_METHOD' o atomize_elim_tac),
+  [("atomize_elim", Method.ctxt_args (SIMPLE_METHOD' o atomize_elim_tac),
     "convert obtains statement to atomic object logic goal")]
   #> AtomizeElimData.setup
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Tools/coherent.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -225,7 +225,7 @@
     end) context 1) ctxt;
 
 fun coherent_meth rules ctxt =
-  Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
+  METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
 
 val setup = Method.add_method
   ("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula");
diff -r e19d5b459a61 -r 4120fc59dd85 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Tools/eqsubst.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -434,7 +434,7 @@
 (* inthms are the given arguments in Isar, and treated as eqstep with
    the first one, then the second etc *)
 fun eqsubst_meth ctxt occL inthms =
-    Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
+    SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
 
 (* apply a substitution inside assumption j, keeps asm in the same place *)
 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
@@ -548,7 +548,7 @@
 (* inthms are the given arguments in Isar, and treated as eqstep with
    the first one, then the second etc *)
 fun eqsubst_asm_meth ctxt occL inthms =
-    Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
+    SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
 
 (* syntax for options, given "(asm)" will give back true, without
    gives back false *)
diff -r e19d5b459a61 -r 4120fc59dd85 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Tools/induct.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -738,20 +738,20 @@
 fun cases_meth src =
   Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
   #> (fn ((insts, opt_rule), ctxt) =>
-    Method.METHOD_CASES (fn facts =>
+    METHOD_CASES (fn facts =>
       Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
 
 fun induct_meth src =
   Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
     (arbitrary -- taking -- Scan.option induct_rule)) src
   #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
-    Method.RAW_METHOD_CASES (fn facts =>
+    RAW_METHOD_CASES (fn facts =>
       Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
 
 fun coinduct_meth src =
   Method.syntax (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule) src
   #> (fn (((insts, taking), opt_rule), ctxt) =>
-    Method.RAW_METHOD_CASES (fn facts =>
+    RAW_METHOD_CASES (fn facts =>
       Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
 
 end;
diff -r e19d5b459a61 -r 4120fc59dd85 src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Tools/intuitionistic.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -86,7 +86,7 @@
 
 val method =
   Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
-    (fn n => fn prems => fn ctxt => Method.METHOD (fn facts =>
+    (fn n => fn prems => fn ctxt => METHOD (fn facts =>
       HEADGOAL (Method.insert_tac (prems @ facts) THEN'
       ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
 
diff -r e19d5b459a61 -r 4120fc59dd85 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/ZF/Tools/typechk.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -116,7 +116,7 @@
   Method.only_sectioned_args
     [Args.add -- Args.colon >> K (I, TC_add),
      Args.del -- Args.colon >> K (I, TC_del)]
-  (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
+  (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
 
 val _ =
   OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
diff -r e19d5b459a61 -r 4120fc59dd85 src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -496,13 +496,11 @@
 setup ProgramDefs.setup
 
 method_setup safety = {*
-  Method.ctxt_args (fn ctxt =>
-    Method.SIMPLE_METHOD' (constrains_tac ctxt)) *}
+  Method.ctxt_args (SIMPLE_METHOD' o constrains_tac) *}
   "for proving safety properties"
 
 method_setup always = {*
-  Method.ctxt_args (fn ctxt =>
-    Method.SIMPLE_METHOD' (always_tac ctxt)) *}
+  Method.ctxt_args (SIMPLE_METHOD' o always_tac) *}
   "for proving invariants"
 
 end