# HG changeset patch
# User wenzelm
# Date 1236984605 -3600
# Node ID bca05b17b6186a6829ac8fe9c22f8f50872089e9
# Parent  9455ecc7796d8b54b1cbde9be508c9aad19c85f8
simplified method setup;

diff -r 9455ecc7796d -r bca05b17b618 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/CCL/Wfd.thy	Fri Mar 13 23:50:05 2009 +0100
@@ -504,8 +504,9 @@
 
 val eval_setup =
   Data.setup #>
-  Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
-    SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")];
+  Method.setup @{binding eval}
+    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))))
+    "evaluation";
 
 end;
 
diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -72,8 +72,8 @@
 (** Setup **)
 
 val setup =
-  Method.add_methods [("algebra", Method.ctxt_args (SIMPLE_METHOD' o algebra_tac),
-    "normalisation of algebraic structure")] #>
+  Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
+    "normalisation of algebraic structure" #>
   Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
 
 end;
diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Orderings.thy	Fri Mar 13 23:50:05 2009 +0100
@@ -397,8 +397,7 @@
 (** Setup **)
 
 val setup =
-  Method.add_methods
-    [("order", Method.ctxt_args (SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
+  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
   Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
 
 end;
diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Tools/function_package/auto_term.ML
--- a/src/HOL/Tools/function_package/auto_term.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/function_package/auto_term.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -29,8 +29,9 @@
     TRY (FundefCommon.apply_termination_rule ctxt i)
     THEN PRIMITIVE (inst_thm ctxt rel)
 
-val setup = Method.add_methods
-  [("relation", (SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
-    "proves termination using a user-specified wellfounded relation")]
+val setup =
+  Method.setup @{binding relation}
+    (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
+    "proves termination using a user-specified wellfounded relation"
 
 end
diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -300,8 +300,8 @@
     end
 
 val setup =
-    Method.add_methods [("pat_completeness", Method.ctxt_args pat_completeness, 
-                         "Completeness prover for datatype patterns")]
+    Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
+        "Completeness prover for datatype patterns"
     #> Context.theory_map (FundefCommon.set_preproc sequential_preproc)
 
 
diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Tools/function_package/induction_scheme.ML
--- a/src/HOL/Tools/function_package/induction_scheme.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/function_package/induction_scheme.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -398,8 +398,8 @@
 fun induct_scheme_tac ctxt =
   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 (RAW_METHOD o induct_scheme_tac),
-    "proves an induction principle")]
+val setup =
+  Method.setup @{binding induct_scheme} (Scan.succeed (RAW_METHOD o induct_scheme_tac))
+    "proves an induction principle"
 
 end
diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -460,9 +460,10 @@
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
 
 
-fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source --
-    Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) [])) src
-  #> (fn ((raw_props, fixes), ctxt) =>
+val ind_cases =
+  Scan.lift (Scan.repeat1 Args.name_source --
+    Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
+  (fn (raw_props, fixes) => fn ctxt =>
     let
       val (_, ctxt') = Variable.add_fixes fixes ctxt;
       val props = Syntax.read_props ctxt' raw_props;
@@ -933,8 +934,7 @@
 (* setup theory *)
 
 val setup =
-  Method.add_methods [("ind_cases", ind_cases,
-    "dynamic case analysis on predicates")] #>
+  Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
   Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
     "declaration of monotonicity rule")];
 
diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -912,9 +912,8 @@
   ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false,
   more_arith_tacs ctxt];
 
-fun arith_method src =
-  Method.syntax Args.bang_facts src
-  #> (fn (prems, ctxt) => METHOD (fn facts =>
+val arith_method = Args.bang_facts >>
+  (fn prems => fn ctxt => METHOD (fn facts =>
       HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
       THEN' arith_tac ctxt)));
 
@@ -930,8 +929,7 @@
       (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
   Context.mapping
    (setup_options #>
-    Method.add_methods
-      [("arith", arith_method, "decide linear arithmetic")] #>
+    Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
     Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
       "declaration of split rules for arithmetic procedure")]) I;
 
diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -637,17 +637,16 @@
   val metisF_tac = metis_general_tac ResAtp.Fol;
   val metisH_tac = metis_general_tac ResAtp.Hol;
 
-  fun method mode = Method.thms_ctxt_args (fn ths => fn ctxt =>
-    SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths));
+  fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
+    SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
 
   val setup =
     type_lits_setup #>
-    Method.add_methods
-      [("metis", method ResAtp.Auto, "METIS for FOL & HOL problems"),
-       ("metisF", method ResAtp.Fol, "METIS for FOL problems"),
-       ("metisH", method ResAtp.Hol, "METIS for HOL problems"),
-       ("finish_clausify",
-         Method.no_args (SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
-    "cleanup after conversion to clauses")];
+    method @{binding metis} ResAtp.Auto "METIS for FOL & HOL problems" #>
+    method @{binding metisF} ResAtp.Fol "METIS for FOL problems" #>
+    method @{binding metisH} ResAtp.Hol "METIS for HOL problems" #>
+    Method.setup @{binding finish_clausify}
+      (Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl))))
+      "cleanup after conversion to clauses";
 
 end;
diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -487,10 +487,10 @@
     val thy = Thm.theory_of_thm st0
   in  (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
 
-val meson_method_setup = Method.add_methods
-  [("meson", Method.thms_args (fn ths =>
-      SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
-    "MESON resolution proof procedure")];
+val meson_method_setup =
+  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn _ =>
+    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)))
+    "MESON resolution proof procedure";
 
 
 (*** Converting a subgoal into negated conjecture clauses. ***)
@@ -521,9 +521,9 @@
           REPEAT_DETERM_N (length ts) o (etac thin_rl)]
      end);
 
-val setup_methods = Method.add_methods
-  [("neg_clausify", Method.no_args (SIMPLE_METHOD' neg_clausify_tac),
-    "conversion of goal to conjecture clauses")];
+val setup_methods =
+  Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac)))
+  "conversion of goal to conjecture clauses";
 
 
 (** Attribute for converting a theorem into clauses **)
diff -r 9455ecc7796d -r bca05b17b618 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Provers/hypsubst.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -284,9 +284,10 @@
 (* theory setup *)
 
 val hypsubst_setup =
-  Method.add_methods
-    [("hypsubst", Method.no_args (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
-        "substitution using an assumption (improper)"),
-     ("simplesubst", Method.thm_args (SIMPLE_METHOD' o stac), "simple substitution")];
+  Method.setup @{binding hypsubst}
+    (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
+    "substitution using an assumption (improper)" #>
+  Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
+    "simple substitution";
 
 end;
diff -r 9455ecc7796d -r bca05b17b618 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Provers/splitter.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -472,16 +472,15 @@
   Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
   Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
 
-fun split_meth src =
-  Method.syntax Attrib.thms src
-  #> (fn (ths, _) => SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
+val split_meth = Attrib.thms >>
+  (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)));
 
 
 (* theory setup *)
 
 val setup =
- (Attrib.add_attributes
-  [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
-  Method.add_methods [(splitN, split_meth, "apply case split rule")]);
+  Attrib.add_attributes
+    [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
+  Method.setup @{binding split} split_meth "apply case split rule";
 
 end;
diff -r 9455ecc7796d -r bca05b17b618 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -615,11 +615,10 @@
     default_intro_tac ctxt facts;
 
 val _ = Context.>> (Context.map_theory
-  (Method.add_methods
-   [("intro_classes", Method.no_args (METHOD intro_classes_tac),
-      "back-chain introduction rules of classes"),
-    ("default", Method.thms_ctxt_args (METHOD oo default_tac),
-      "apply some intro/elim rule")]));
+ (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
+    "back-chain introduction rules of classes" #>
+  Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
+    "apply some intro/elim rule"));
 
 end;
 
diff -r 9455ecc7796d -r bca05b17b618 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -487,13 +487,10 @@
     (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
 
 val _ = Context.>> (Context.map_theory
-  (Method.add_methods
-    [("intro_locales",
-      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 (intro_locales_tac true ctxt)),
-      "back-chain all introduction rules of locales")]));
+ (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
+    "back-chain introduction rules of locales without unfolding predicates" #>
+  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
+    "back-chain all introduction rules of locales"));
 
 end;
 
diff -r 9455ecc7796d -r bca05b17b618 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Pure/Isar/method.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -456,18 +456,22 @@
 end;
 
 
+(* extra rule methods *)
+
+fun xrule_meth m =
+  Scan.lift (Scan.optional (Args.parens OuterParse.nat) 0) -- Attrib.thms >>
+  (fn (n, ths) => K (m n ths));
+
+
 (* tactic syntax *)
 
-fun nat_thms_args f = uncurry f oo
-  (fst oo syntax (Scan.lift (Scan.optional (Args.parens P.nat) 0) -- Attrib.thms));
-
-fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec HEADGOAL -- args >>
+fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec -- args >>
   (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt);
 
 fun goal_args args tac = goal_args' (Scan.lift args) tac;
 
 fun goal_args_ctxt' args tac src ctxt =
-  fst (syntax (Args.goal_spec HEADGOAL -- args >>
+  fst (syntax (Args.goal_spec -- args >>
   (fn (quant, s) => SIMPLE_METHOD'' quant (tac ctxt s))) src ctxt);
 
 fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
@@ -500,31 +504,38 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
-  (add_methods
-   [("fail", no_args fail, "force failure"),
-    ("succeed", no_args succeed, "succeed"),
-    ("-", no_args insert_facts, "do nothing (insert current facts only)"),
-    ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
-    ("intro", thms_args intro, "repeatedly apply introduction rules"),
-    ("elim", thms_args elim, "repeatedly apply elimination rules"),
-    ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
-    ("fold", thms_ctxt_args fold_meth, "fold definitions"),
-    ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
-      "present local premises as object-level statements"),
-    ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
-    ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
-    ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
-    ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
-    ("this", no_args this, "apply current facts as rules"),
-    ("fact", thms_ctxt_args fact, "composition by facts from context"),
-    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
-    ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_tac,
-      "rename parameters of goal"),
-    ("rotate_tac", goal_args (Scan.optional P.int 1) Tactic.rotate_tac,
-      "rotate assumptions of goal"),
-    ("tactic", simple_args (P.position Args.name) tactic, "ML tactic as proof method"),
-    ("raw_tactic", simple_args (P.position Args.name) raw_tactic,
-      "ML tactic as raw proof method")]));
+ (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
+  setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
+  setup (Binding.name "-") (Scan.succeed (K insert_facts))
+    "do nothing (insert current facts only)" #>
+  setup (Binding.name "insert") (Attrib.thms >> (K o insert))
+    "insert theorems, ignoring facts (improper)" #>
+  setup (Binding.name "intro") (Attrib.thms >> (K o intro))
+    "repeatedly apply introduction rules" #>
+  setup (Binding.name "elim") (Attrib.thms >> (K o elim))
+    "repeatedly apply elimination rules" #>
+  setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
+  setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
+  setup (Binding.name "atomize") (Args.mode "full" >> (K o atomize))
+    "present local premises as object-level statements" #>
+  setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #>
+  setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
+  setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
+  setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
+  setup (Binding.name "this") (Scan.succeed (K this)) "apply current facts as rules" #>
+  setup (Binding.name "fact") (Attrib.thms >> fact) "composition by facts from context" #>
+  setup (Binding.name "assumption") (Scan.succeed assumption)
+    "proof by assumption, preferring facts" #>
+  setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
+    (fn (quant, xs) => K (SIMPLE_METHOD'' quant (Tactic.rename_tac xs))))
+    "rename parameters of goal" #>
+  setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional P.int 1) >>
+    (fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
+      "rotate assumptions of goal" #>
+  setup (Binding.name "tactic") (Scan.lift (P.position Args.name) >> tactic)
+    "ML tactic as proof method" #>
+  setup (Binding.name "raw_tactic") (Scan.lift (P.position Args.name) >> raw_tactic)
+    "ML tactic as raw proof method"));
 
 
 (*final declarations of this structure!*)
diff -r 9455ecc7796d -r bca05b17b618 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -386,61 +386,48 @@
 
 local
 
-fun gen_inst _ tac _ (quant, ([], thms)) =
-      METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
-  | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
-      METHOD (fn facts =>
-        quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm))
-  | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
+fun inst_meth inst_tac tac =
+  Args.goal_spec --
+  Scan.optional (Scan.lift
+    (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
+  Attrib.thms >>
+  (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
+    if null insts then quant (Method.insert_tac facts THEN' tac thms)
+    else
+      (case thms of
+        [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
+      | _ => error "Cannot have instantiations with multiple rules")));
 
 in
 
-val res_inst_meth = gen_inst res_inst_tac Tactic.resolve_tac;
-val eres_inst_meth = gen_inst eres_inst_tac Tactic.eresolve_tac;
-val cut_inst_meth = gen_inst cut_inst_tac Tactic.cut_rules_tac;
-val dres_inst_meth = gen_inst dres_inst_tac Tactic.dresolve_tac;
-val forw_inst_meth = gen_inst forw_inst_tac Tactic.forward_tac;
+val res_inst_meth = inst_meth res_inst_tac Tactic.resolve_tac;
+val eres_inst_meth = inst_meth eres_inst_tac Tactic.eresolve_tac;
+val cut_inst_meth = inst_meth cut_inst_tac Tactic.cut_rules_tac;
+val dres_inst_meth = inst_meth dres_inst_tac Tactic.dresolve_tac;
+val forw_inst_meth = inst_meth forw_inst_tac Tactic.forward_tac;
 
 end;
 
 
-(* method syntax *)
-
-val insts =
-  Scan.optional (Scan.lift
-    (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
-    -- Attrib.thms;
-
-fun inst_args f src ctxt =
-  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
-
-val insts_var =
-  Scan.optional (Scan.lift
-    (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
-    -- Attrib.thms;
-
-fun inst_args_var f src ctxt =
-  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
-
-
 (* setup *)
 
 val _ = Context.>> (Context.map_theory
-  (Method.add_methods
-   [("rule_tac", inst_args_var res_inst_meth,
-      "apply rule (dynamic instantiation)"),
-    ("erule_tac", inst_args_var eres_inst_meth,
-      "apply rule in elimination manner (dynamic instantiation)"),
-    ("drule_tac", inst_args_var dres_inst_meth,
-      "apply rule in destruct manner (dynamic instantiation)"),
-    ("frule_tac", inst_args_var forw_inst_meth,
-      "apply rule in forward manner (dynamic instantiation)"),
-    ("cut_tac", inst_args_var cut_inst_meth,
-      "cut rule (dynamic instantiation)"),
-    ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name_source) subgoals_tac,
-      "insert subgoal (dynamic instantiation)"),
-    ("thin_tac", Method.goal_args_ctxt Args.name_source thin_tac,
-      "remove premise (dynamic instantiation)")]));
+ (Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
+  Method.setup (Binding.name "erule_tac") eres_inst_meth
+    "apply rule in elimination manner (dynamic instantiation)" #>
+  Method.setup (Binding.name "drule_tac") dres_inst_meth
+    "apply rule in destruct manner (dynamic instantiation)" #>
+  Method.setup (Binding.name "frule_tac") forw_inst_meth
+    "apply rule in forward manner (dynamic instantiation)" #>
+  Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #>
+  Method.setup (Binding.name "subgoal_tac")
+    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
+      (fn (quant, props) => fn ctxt => SIMPLE_METHOD'' quant (subgoals_tac ctxt props)))
+    "insert subgoal (dynamic instantiation)" #>
+  Method.setup (Binding.name "thin_tac")
+    (Args.goal_spec -- Scan.lift Args.name_source >>
+      (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
+      "remove premise (dynamic instantiation)"));
 
 end;
 
diff -r 9455ecc7796d -r bca05b17b618 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Tools/atomize_elim.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -131,9 +131,9 @@
       THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
     end)
 
-val setup = Method.add_methods
-  [("atomize_elim", Method.ctxt_args (SIMPLE_METHOD' o atomize_elim_tac),
-    "convert obtains statement to atomic object logic goal")]
+val setup =
+  Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
+    "convert obtains statement to atomic object logic goal"
   #> AtomizeElimData.setup
 
 end
diff -r 9455ecc7796d -r bca05b17b618 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Tools/induct.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -735,22 +735,21 @@
 
 in
 
-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_CASES (fn facts =>
-      Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
+val cases_meth =
+  P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
+  (fn (insts, opt_rule) => fn ctxt =>
+    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) =>
+val induct_meth =
+  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+    (arbitrary -- taking -- Scan.option induct_rule) >>
+  (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
     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) =>
+val coinduct_meth =
+  Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
+  (fn ((insts, taking), opt_rule) => fn ctxt =>
     RAW_METHOD_CASES (fn facts =>
       Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
 
@@ -762,9 +761,8 @@
 
 val setup =
   attrib_setup #>
-  Method.add_methods
-    [(casesN, cases_meth, "case analysis on types or predicates/sets"),
-     (inductN, induct_meth, "induction on types or predicates/sets"),
-     (coinductN, coinduct_meth, "coinduction on types or predicates/sets")];
+  Method.setup @{binding cases} cases_meth "case analysis on types or predicates/sets" #>
+  Method.setup @{binding induct} induct_meth "induction on types or predicates/sets" #>
+  Method.setup @{binding coinduct} coinduct_meth "coinduction on types or predicates/sets";
 
 end;
diff -r 9455ecc7796d -r bca05b17b618 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -57,19 +57,14 @@
 
 (* ind_cases method *)
 
-fun mk_cases_meth (props, ctxt) =
-  props
-  |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
-  |> Method.erule 0;
-
-val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name_source));
-
-
-(* package setup *)
+val mk_cases_meth = Scan.lift (Scan.repeat1 Args.name_source) >>
+  (fn props => fn ctxt =>
+    props
+    |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
+    |> Method.erule 0);
 
 val setup =
-  Method.add_methods
-    [("ind_cases", mk_cases_meth oo mk_cases_args, "dynamic case analysis on sets")];
+  Method.setup @{binding "ind_cases"} mk_cases_meth "dynamic case analysis on sets";
 
 
 (* outer syntax *)