# HG changeset patch
# User wenzelm
# Date 1237224270 -3600
# Node ID d2d7874648bda047741356da04c9ead1290ff72c
# Parent  2eef5e71edd6bfebb3fbce2e67c4c5dbc4a6dc7f
simplified method setup;

diff -r 2eef5e71edd6 -r d2d7874648bd src/Cube/Example.thy
--- a/src/Cube/Example.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/Cube/Example.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -15,20 +15,19 @@
 *}
 
 method_setup depth_solve = {*
-  Method.thms_args (fn thms => METHOD (fn facts =>
-  (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
+  Attrib.thms >> (fn thms => K (METHOD (fn facts =>
+  (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
 *} ""
 
 method_setup depth_solve1 = {*
-  Method.thms_args (fn thms => METHOD (fn facts =>
-  (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
+  Attrib.thms >> (fn thms => K (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 (fn facts =>
-      REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
-  end
+  Attrib.thms >> (fn thms => K (METHOD (fn facts =>
+    REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN
+    DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))
 *} ""
 
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/FOL/FOL.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -73,9 +73,10 @@
   fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
 *}
 
-method_setup case_tac =
-  {* Method.goal_args_ctxt Args.name_source case_tac *}
-  "case_tac emulation (dynamic instantiation!)"
+method_setup case_tac = {*
+  Args.goal_spec -- Scan.lift Args.name_source >>
+  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
+*} "case_tac emulation (dynamic instantiation!)"
 
 
 (*** Special elimination rules *)
diff -r 2eef5e71edd6 -r d2d7874648bd src/FOL/ex/Iff_Oracle.thy
--- a/src/FOL/ex/Iff_Oracle.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/FOL/ex/Iff_Oracle.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -52,7 +52,7 @@
 subsection {* Oracle as proof method *}
 
 method_setup iff = {*
-  Method.simple_args OuterParse.nat (fn n => fn ctxt =>
+  Scan.lift OuterParse.nat >> (fn n => fn ctxt =>
     SIMPLE_METHOD
       (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
         handle Fail _ => no_tac))
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -222,7 +222,7 @@
 *}   (* Note: r_one is not necessary in ring_ss *)
 
 method_setup ring =
-  {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss))) *}
   {* computes distributive normal form in rings *}
 
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/Event.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -289,7 +289,7 @@
 *}
 
 method_setup analz_mono_contra = {*
-    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+    Scan.succeed (K (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 (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
+    Scan.succeed (K (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 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/Message.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -941,15 +941,15 @@
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
 
 method_setup spy_analz = {*
-    Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
+    Scan.succeed (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 (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
+    Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
     "for debugging spy_analz"
 
 method_setup Fake_insert_simp = {*
-    Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
+    Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
     "for debugging spy_analz"
 
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/OtwayReesBella.thy
--- a/src/HOL/Auth/OtwayReesBella.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/OtwayReesBella.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -137,7 +137,7 @@
 *}
  
 method_setup parts_explicit = {*
-    Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *}
+    Scan.succeed (K (SIMPLE_METHOD' parts_explicit_tac)) *}
   "to explicitly state that some message components belong to parts knows Spy"
 
 
@@ -257,7 +257,7 @@
 *}
 
 method_setup analz_freshCryptK = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
@@ -267,10 +267,10 @@
 
 
 method_setup disentangle = {*
-    Method.no_args
-     (SIMPLE_METHOD
+    Scan.succeed
+     (K (SIMPLE_METHOD
       (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
-                   ORELSE' hyp_subst_tac))) *}
+                   ORELSE' hyp_subst_tac)))) *}
   "for eliminating conjunctions, disjunctions and the like"
 
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/Public.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -424,7 +424,7 @@
 *}
 
 method_setup analz_freshK = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
@@ -435,11 +435,11 @@
 subsection{*Specialized Methods for Possibility Theorems*}
 
 method_setup possibility = {*
-    Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *}
+    Scan.succeed (SIMPLE_METHOD o Public.possibility_tac) *}
     "for proving possibility theorems"
 
 method_setup basic_possibility = {*
-    Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *}
+    Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac) *}
     "for proving possibility theorems"
 
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/Shared.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -238,7 +238,7 @@
 (*Specialized methods*)
 
 method_setup analz_freshK = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
@@ -246,11 +246,11 @@
     "for proving the Session Key Compromise theorem"
 
 method_setup possibility = {*
-    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
     "for proving possibility theorems"
 
 method_setup basic_possibility = {*
-    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
+    Scan.succeed (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 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/Smartcard/ShoupRubin.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -769,15 +769,15 @@
 *}
 
 method_setup prepare = {*
-    Method.no_args (SIMPLE_METHOD ShoupRubin.prepare_tac) *}
+    Scan.succeed (K (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 => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
   "additional facts to reason about parts"
 
 method_setup analz_prepare = {*
-    Method.no_args (SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
+    Scan.succeed (K (SIMPLE_METHOD ShoupRubin.analz_prepare_tac)) *}
   "additional facts to reason about analz"
 
 
@@ -822,7 +822,7 @@
 done
 
 method_setup sc_analz_freshK = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST
        (resolve_tac [allI, ballI, impI]),
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/Smartcard/ShoupRubinBella.thy
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -777,15 +777,15 @@
 *}
 
 method_setup prepare = {*
-    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
+    Scan.succeed (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 => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
   "additional facts to reason about parts"
 
 method_setup analz_prepare = {*
-    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
   "additional facts to reason about analz"
 
 
@@ -831,7 +831,7 @@
 done
 
 method_setup sc_analz_freshK = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -407,7 +407,7 @@
 (*Specialized methods*)
 
 method_setup analz_freshK = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
@@ -415,12 +415,12 @@
     "for proving the Session Key Compromise theorem"
 
 method_setup possibility = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
         SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
     "for proving possibility theorems"
 
 method_setup basic_possibility = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
         SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
     "for proving possibility theorems"
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Code_Setup.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -226,19 +226,19 @@
 *}
 
 ML {*
-fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD'
+fun gen_eval_method conv ctxt = SIMPLE_METHOD'
   (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
-    THEN' rtac TrueI))
+    THEN' rtac TrueI)
 *}
 
-method_setup eval = {* gen_eval_method eval_oracle *}
+method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
   "solve goal by evaluation"
 
-method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
+method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
   "solve goal by evaluation"
 
-method_setup normalization = {* (Method.no_args o SIMPLE_METHOD')
-  (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
+method_setup normalization = {*
+  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
 *} "solve goal by normalization"
 
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -2496,16 +2496,15 @@
 
 *}
 
-method_setup approximation = {* fn src => 
-  Method.syntax Args.term src #>
-  (fn (prec, ctxt) => let
-   in SIMPLE_METHOD' (fn i =>
+method_setup approximation = {*
+  Args.term >>
+  (fn prec => fn ctxt =>
+    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 
       THEN (TRY (filter_prems_tac (fn t => false) i))
-      THEN (gen_eval_tac eval_oracle ctxt) i))
-   end)
+      THEN (gen_eval_tac eval_oracle ctxt) i)))
 *} "real number approximation"
  
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -295,7 +295,7 @@
 
 use "~~/src/HOL/Tools/Qelim/langford.ML"
 method_setup dlo = {*
-  Method.ctxt_args (SIMPLE_METHOD' o LangfordQE.dlo_tac)
+  Scan.succeed (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 (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
+  Scan.succeed (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 2eef5e71edd6 -r d2d7874648bd src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -253,7 +253,7 @@
 
 
 method_setup sring_norm = {*
-  Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
+  Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
 *} "semiring normalizer"
 
 
@@ -427,10 +427,9 @@
  val any_keyword = keyword addN || keyword delN
  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
 in
-fn src => Method.syntax 
-    ((Scan.optional (keyword addN |-- thms) []) -- 
-    (Scan.optional (keyword delN |-- thms) [])) src 
- #> (fn ((add_ths, del_ths), ctxt) => 
+  ((Scan.optional (keyword addN |-- thms) []) -- 
+   (Scan.optional (keyword delN |-- thms) [])) >>
+  (fn (add_ths, del_ths) => fn ctxt =>
        SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
 end
 *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -234,11 +234,11 @@
 use "hoare_tac.ML"
 
 method_setup vcg = {*
-  Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
   "verification condition generator"
 
 method_setup vcg_simp = {*
-  Method.ctxt_args (fn ctxt =>
+  Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   "verification condition generator plus simplification"
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Hoare/HoareAbort.thy
--- a/src/HOL/Hoare/HoareAbort.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -246,11 +246,11 @@
 use "hoare_tac.ML"
 
 method_setup vcg = {*
-  Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
   "verification condition generator"
 
 method_setup vcg_simp = {*
-  Method.ctxt_args (fn ctxt =>
+  Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   "verification condition generator plus simplification"
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/HoareParallel/OG_Tactics.thy
--- a/src/HOL/HoareParallel/OG_Tactics.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/HoareParallel/OG_Tactics.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -465,21 +465,21 @@
 Isabelle proofs. *}
 
 method_setup oghoare = {*
-  Method.no_args (SIMPLE_METHOD' oghoare_tac) *}
+  Scan.succeed (K (SIMPLE_METHOD' oghoare_tac)) *}
   "verification condition generator for the oghoare logic"
 
 method_setup annhoare = {*
-  Method.no_args (SIMPLE_METHOD' annhoare_tac) *}
+  Scan.succeed (K (SIMPLE_METHOD' annhoare_tac)) *}
   "verification condition generator for the ann_hoare logic"
 
 method_setup interfree_aux = {*
-  Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *}
+  Scan.succeed (K (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 (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
+  Scan.succeed (K (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 (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
+  Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac)))) *}
   "verification condition generator for interference freedom tests"
 
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -454,7 +454,7 @@
 use "~~/src/HOL/Hoare/hoare_tac.ML"
 
 method_setup hoare = {*
-  Method.ctxt_args (fn ctxt =>
+  Scan.succeed (fn ctxt =>
     (SIMPLE_METHOD'
        (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}
   "verification condition generator for Hoare logic"
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -134,8 +134,8 @@
    (* 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 (SIMPLE_METHOD' o vector_arith_tac)
-end
+  Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
+ end
 *} "Lifts trivial vector statements to real arith statements"
 
 lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
@@ -948,7 +948,7 @@
 
 use "normarith.ML"
 
-method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
+method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
 *} "Proves simple linear statements about vector norms"
 
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/Library/Eval_Witness.thy
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
-
 *)
 
 header {* Evaluation Oracle with ML witnesses *}
@@ -78,15 +76,10 @@
 
 
 method_setup eval_witness = {*
-let
-
-fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
-
-in
-  Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
-    SIMPLE_METHOD' (eval_tac ws))
-end
-*} "Evaluation with ML witnesses"
+  Scan.lift (Scan.repeat Args.name) >>
+  (fn ws => K (SIMPLE_METHOD'
+    (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
+*} "evaluation with ML witnesses"
 
 
 subsection {* Toy Examples *}
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Library/Reflection.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -16,10 +16,10 @@
 
 use "reflection.ML"
 
-method_setup reify = {* fn src =>
-  Method.syntax (Attrib.thms --
-    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
-  (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
+method_setup reify = {*
+  Attrib.thms --
+    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
+  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
 *} "partial automatic reification"
 
 method_setup reflection = {* 
@@ -30,16 +30,17 @@
   val any_keyword = keyword onlyN || keyword rulesN;
   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   val terms = thms >> map (term_of o Drule.dest_term);
-  fun optional scan = Scan.optional scan [];
-in fn src =>
-  Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
-    (fn (((eqs,ths),to), ctxt) => 
-      let 
-        val (ceqs,cths) = Reify_Data.get ctxt 
-        val corr_thms = ths@cths
-        val raw_eqs = eqs@ceqs
-      in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
-     end) end
-*} "reflection method"
+in
+  thms --
+  Scan.optional (keyword rulesN |-- thms) [] --
+  Scan.option (keyword onlyN |-- Args.term) >>
+  (fn ((eqs,ths),to) => fn ctxt =>
+    let 
+      val (ceqs,cths) = Reify_Data.get ctxt 
+      val corr_thms = ths@cths
+      val raw_eqs = eqs@ceqs
+    in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
+end
+*} "reflection"
 
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -978,9 +978,8 @@
   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 (SIMPLE_METHOD' o tac) end
-
-*} "Reduces goals about net"
+  in Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (tac ths))) end
+*} "reduces goals about net"
 
 lemma at: "\<And>x y. netord (at a) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a <= dist y a"
   apply (net at_def)
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Mar 16 18:24:30 2009 +0100
@@ -199,9 +199,10 @@
     (Args.parens (Args.$$$ "no_asm") >> (K true)) ||
      (Scan.succeed false);
 
-val setup_generate_fresh =
-  Method.goal_args_ctxt' Args.tyname (fn ctxt => generate_fresh_tac) 
+fun setup_generate_fresh x =
+  (Args.goal_spec -- Args.tyname >>
+    (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
 
-val setup_fresh_fun_simp =
-  Method.simple_args options_syntax 
-  (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1))
+fun setup_fresh_fun_simp x =
+  (Scan.lift options_syntax >> (fn b => K (SIMPLE_METHOD' (fresh_fun_tac b)))) x;
+
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Mon Mar 16 18:24:30 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 -> Proof.method
+  val nominal_induct_method: (Proof.context -> Proof.method) context_parser
 end =
 struct
 
@@ -152,11 +152,10 @@
 
 in
 
-fun nominal_induct_method src =
-  Method.syntax
-   (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
-    avoiding -- fixing -- rule_spec) src
-  #> (fn ((((x, y), z), w), ctxt) =>
+val nominal_induct_method =
+  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+  avoiding -- fixing -- rule_spec >>
+  (fn (((x, y), z), w) => fn ctxt =>
     RAW_METHOD_CASES (fn facts =>
       HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Mar 16 18:24:30 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Nominal/nominal_permeq.ML
-    ID:         $Id$
     Authors:    Christian Urban, Julien Narboux, TU Muenchen
 
 Methods for simplifying permutations and
@@ -36,16 +35,16 @@
   val finite_guess_tac : simpset -> int -> tactic
   val fresh_guess_tac : simpset -> int -> tactic
 
-  val perm_simp_meth : Method.src -> Proof.context -> Proof.method
-  val perm_simp_meth_debug : Method.src -> Proof.context -> Proof.method
-  val perm_extend_simp_meth : Method.src -> Proof.context -> Proof.method
-  val perm_extend_simp_meth_debug : Method.src -> Proof.context -> Proof.method
-  val supports_meth : Method.src -> Proof.context -> Proof.method
-  val supports_meth_debug : Method.src -> Proof.context -> Proof.method
-  val finite_guess_meth : Method.src -> Proof.context -> Proof.method
-  val finite_guess_meth_debug : Method.src -> Proof.context -> Proof.method
-  val fresh_guess_meth : Method.src -> Proof.context -> Proof.method
-  val fresh_guess_meth_debug : Method.src -> Proof.context -> Proof.method
+  val perm_simp_meth : (Proof.context -> Proof.method) context_parser
+  val perm_simp_meth_debug : (Proof.context -> Proof.method) context_parser
+  val perm_extend_simp_meth : (Proof.context -> Proof.method) context_parser
+  val perm_extend_simp_meth_debug : (Proof.context -> Proof.method) context_parser
+  val supports_meth : (Proof.context -> Proof.method) context_parser
+  val supports_meth_debug : (Proof.context -> Proof.method) context_parser
+  val finite_guess_meth : (Proof.context -> Proof.method) context_parser
+  val finite_guess_meth_debug : (Proof.context -> Proof.method) context_parser
+  val fresh_guess_meth : (Proof.context -> Proof.method) context_parser
+  val fresh_guess_meth_debug : (Proof.context -> Proof.method) context_parser
 end
 
 structure NominalPermeq : NOMINAL_PERMEQ =
@@ -400,26 +399,24 @@
   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 (fn facts =>
-   HEADGOAL (Method.insert_tac (prems @ facts) THEN'
-       ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
-
-val perm_simp_meth = Method.sectioned_args
-     (Args.bang_facts -- Scan.lift perm_simp_options)
-     (Simplifier.simp_modifiers') perm_simp_method
+val perm_simp_meth =
+  Args.bang_facts -- Scan.lift perm_simp_options --|
+  Method.sections (Simplifier.simp_modifiers') >>
+  (fn (prems, tac) => fn ctxt => METHOD (fn facts =>
+    HEADGOAL (Method.insert_tac (prems @ facts) THEN'
+      (CHANGED_PROP oo tac) (local_simpset_of ctxt))));
 
 (* 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)
-  (SIMPLE_METHOD' o tac o local_simpset_of) ;
+  Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
+  (K (SIMPLE_METHOD' o tac o local_simpset_of));
 
 (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
 
 fun basic_simp_meth_setup debug tac =
-  Method.sectioned_args 
-   (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
-   (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
-   (fn _ => SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
+  Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ())) --
+  Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
+  (K (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 2eef5e71edd6 -r d2d7874648bd src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Presburger.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -455,12 +455,11 @@
  val any_keyword = keyword addN || keyword delN || simple_keyword elimN
  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
 in
-  fn src => Method.syntax 
-   ((Scan.optional (simple_keyword elimN >> K false) true) -- 
-    (Scan.optional (keyword addN |-- thms) []) -- 
-    (Scan.optional (keyword delN |-- thms) [])) src 
-  #> (fn (((elim, add_ths), del_ths),ctxt) => 
-         SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
+  Scan.optional (simple_keyword elimN >> K false) true --
+  Scan.optional (keyword addN |-- thms) [] --
+  Scan.optional (keyword delN |-- thms) [] >>
+  (fn ((elim, add_ths), del_ths) => fn ctxt =>
+    SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
 end
 *} "Cooper's algorithm for Presburger arithmetic"
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Prolog/HOHH.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -11,11 +11,11 @@
 begin
 
 method_setup ptac =
-  {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
+  {* Attrib.thms >> (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 => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
+  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
   "Lambda Prolog interpreter"
 
 consts
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/SAT.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/SAT.thy
-    ID:         $Id$
     Author:     Alwen Tiu, Tjark Weber
     Copyright   2005
 
@@ -28,10 +27,10 @@
 
 ML {* structure sat = SATFunc(structure cnf = cnf); *}
 
-method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
+method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *}
   "SAT solver"
 
-method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
+method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *}
   "SAT solver (with definitional CNF)"
 
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/SET-Protocol/Cardholder_Registration.thy
--- a/src/HOL/SET-Protocol/Cardholder_Registration.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -541,10 +541,11 @@
 by (blast intro: analz_mono [THEN [2] rev_subsetD])
 
 method_setup valid_certificate_tac = {*
-  Method.goal_args (Scan.succeed ()) (fn () => fn i =>
-    EVERY [ftac @{thm Gets_certificate_valid} i,
-           assume_tac i,
-           etac conjE i, REPEAT (hyp_subst_tac i)])
+  Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
+    (fn i =>
+      EVERY [ftac @{thm Gets_certificate_valid} i,
+             assume_tac i,
+             etac conjE i, REPEAT (hyp_subst_tac i)])))
 *} ""
 
 text{*The @{text "(no_asm)"} attribute is essential, since it retains
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/SET-Protocol/EventSET.thy
--- a/src/HOL/SET-Protocol/EventSET.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/SET-Protocol/EventSET.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -189,7 +189,7 @@
 *}
 
 method_setup analz_mono_contra = {*
-    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
+    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
 
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/SET-Protocol/MessageSET.thy
--- a/src/HOL/SET-Protocol/MessageSET.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -940,17 +940,17 @@
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
 
 method_setup spy_analz = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn 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 =>
+    Scan.succeed (fn 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 =>
+    Scan.succeed (fn ctxt =>
         SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
     "for debugging spy_analz"
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/SET-Protocol/PublicSET.thy
--- a/src/HOL/SET-Protocol/PublicSET.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/SET-Protocol/PublicSET.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -371,7 +371,7 @@
 *}
 
 method_setup possibility = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
         SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
     "for proving possibility theorems"
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/SET-Protocol/Purchase.thy
--- a/src/HOL/SET-Protocol/Purchase.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/SET-Protocol/Purchase.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -477,9 +477,10 @@
 by (frule Gets_imp_Says, auto)
 
 method_setup valid_certificate_tac = {*
-  Method.goal_args (Scan.succeed ()) (fn () => fn i =>
-    EVERY [ftac @{thm Gets_certificate_valid} i,
-           assume_tac i, REPEAT (hyp_subst_tac i)])
+  Args.goal_spec >> (fn quant =>
+    K (SIMPLE_METHOD'' quant (fn i =>
+      EVERY [ftac @{thm Gets_certificate_valid} i,
+             assume_tac i, REPEAT (hyp_subst_tac i)])))
 *} ""
 
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -695,16 +695,16 @@
 (* Optional methods *)
 
 method_setup trancl =
-  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}
   {* simple transitivity reasoner *}
 method_setup rtrancl =
-  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}
   {* simple transitivity reasoner *}
 method_setup tranclp =
-  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}
   {* simple transitivity reasoner (predicate version) *}
 method_setup rtranclp =
-  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}
   {* simple transitivity reasoner (predicate version) *}
 
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -321,7 +321,7 @@
 *}
 
 method_setup record_auto = {*
-  Method.ctxt_args (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
+  Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
 *} ""
 
 lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
@@ -713,7 +713,7 @@
 *}
 
 method_setup rename_client_map = {*
-  Method.ctxt_args (fn ctxt =>
+  Scan.succeed (fn ctxt =>
     SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
 *} ""
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/UNITY/Simple/NSP_Bad.thy
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -124,7 +124,7 @@
 *}
 
 method_setup ns_induct = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
         SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
     "for inductive reasoning about the Needham-Schroeder protocol"
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -10,15 +10,13 @@
 uses "UNITY_tactics.ML" begin
 
 method_setup safety = {*
-    Method.ctxt_args (fn ctxt =>
+    Scan.succeed (fn ctxt =>
         SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
     "for proving safety properties"
 
 method_setup ensures_tac = {*
-    fn args => fn ctxt =>
-        Method.goal_args' (Scan.lift Args.name_source)
-           (ensures_tac (local_clasimpset_of ctxt))
-           args ctxt *}
-    "for proving progress properties"
+  Args.goal_spec -- Scan.lift Args.name_source >>
+  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (local_clasimpset_of ctxt) s))
+*} "for proving progress properties"
 
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Word/WordArith.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -530,7 +530,7 @@
 *}
 
 method_setup uint_arith = 
-  "Method.ctxt_args (SIMPLE_METHOD' o uint_arith_tac)" 
+  {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}
   "solving word arithmetic via integers and arith"
 
 
@@ -1086,7 +1086,7 @@
 *}
 
 method_setup unat_arith = 
-  "Method.ctxt_args (SIMPLE_METHOD' o unat_arith_tac)" 
+  {* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *}
   "solving word arithmetic via natural numbers and arith"
 
 lemma no_plus_overflow_unat_size: 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/ex/Binary.thy	Mon Mar 16 18:24:30 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 (SIMPLE_METHOD'
+  Scan.succeed (K (SIMPLE_METHOD'
     (full_simp_tac
       (HOL_basic_ss
         addsimps @{thms binary_simps}
@@ -183,7 +183,7 @@
           @{simproc binary_nat_less},
           @{simproc binary_nat_diff},
           @{simproc binary_nat_div},
-          @{simproc binary_nat_mod}])))
+          @{simproc binary_nat_mod}]))))
 *} "binary simplification"
 
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/ex/SAT_Examples.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -83,7 +83,7 @@
 ML {* reset quick_and_dirty; *}
 
 method_setup rawsat =
-  {* Method.no_args (SIMPLE_METHOD' sat.rawsat_tac) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' sat.rawsat_tac)) *}
   "SAT solver (no preprocessing)"
 
 (* ML {* Toplevel.profiling := 1; *} *)
diff -r 2eef5e71edd6 -r d2d7874648bd src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/Sequents/ILL.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -146,7 +146,7 @@
 *}
 
 method_setup best_lazy =
-  {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
+  {* Scan.succeed (K (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 (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
+  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} ""
 
 method_setup best_power =
-  {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
+  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} ""
 
 
 (* Some examples from Troelstra and van Dalen *)
diff -r 2eef5e71edd6 -r d2d7874648bd src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/Sequents/LK0.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -240,23 +240,23 @@
 *}
 
 method_setup fast_prop =
-  {* Method.no_args (SIMPLE_METHOD' (fast_tac prop_pack)) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
   "propositional reasoning"
 
 method_setup fast =
-  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_pack)) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
   "classical reasoning"
 
 method_setup fast_dup =
-  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
   "classical reasoning"
 
 method_setup best =
-  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_pack)) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
   "classical reasoning"
 
 method_setup best_dup =
-  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
+  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
   "classical reasoning"
 
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/Sequents/S4.thy
--- a/src/Sequents/S4.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/Sequents/S4.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -45,7 +45,7 @@
 *}
 
 method_setup S4_solve =
-  {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
+  {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} "S4 solver"
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
diff -r 2eef5e71edd6 -r d2d7874648bd src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/Sequents/S43.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -92,8 +92,8 @@
 
 
 method_setup S43_solve = {*
-  Method.no_args (SIMPLE_METHOD
-    (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))
+  Scan.succeed (K (SIMPLE_METHOD
+    (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
 *} "S4 solver"
 
 
diff -r 2eef5e71edd6 -r d2d7874648bd src/Sequents/T.thy
--- a/src/Sequents/T.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/Sequents/T.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -44,7 +44,7 @@
 *}
 
 method_setup T_solve =
-  {* Method.no_args (SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
+  {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver"
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
diff -r 2eef5e71edd6 -r d2d7874648bd src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -496,11 +496,11 @@
 setup ProgramDefs.setup
 
 method_setup safety = {*
-  Method.ctxt_args (SIMPLE_METHOD' o constrains_tac) *}
+  Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
   "for proving safety properties"
 
 method_setup always = {*
-  Method.ctxt_args (SIMPLE_METHOD' o always_tac) *}
+  Scan.succeed (SIMPLE_METHOD' o always_tac) *}
   "for proving invariants"
 
 end
diff -r 2eef5e71edd6 -r d2d7874648bd src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Mon Mar 16 17:51:24 2009 +0100
+++ b/src/ZF/UNITY/SubstAx.thy	Mon Mar 16 18:24:30 2009 +0100
@@ -377,9 +377,8 @@
 *}
 
 method_setup ensures_tac = {*
-    fn args => fn ctxt =>
-        Method.goal_args' (Scan.lift Args.name_source) (ensures_tac ctxt)
-           args ctxt *}
-    "for proving progress properties"
+    Args.goal_spec -- Scan.lift Args.name_source >>
+    (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
+*} "for proving progress properties"
 
 end