# HG changeset patch
# User wenzelm
# Date 1237145158 -3600
# Node ID 9f168bdc468a37a7ba3a2cf9ca9c49f57ea6e856
# Parent  5e2d9604a3d3b9e911baac9537a9ef6e38ff19b2
simplified method setup;

diff -r 5e2d9604a3d3 -r 9f168bdc468a src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Sun Mar 15 20:19:14 2009 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Sun Mar 15 20:25:58 2009 +0100
@@ -220,9 +220,11 @@
 
 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")]
-     #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
+val setup =
+  Method.setup @{binding lexicographic_order}
+    (Method.sections clasimp_modifiers >> (K lexicographic_order))
+    "termination prover for lexicographic orderings"
+  #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
 
 end;
 
diff -r 5e2d9604a3d3 -r 9f168bdc468a src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sun Mar 15 20:19:14 2009 +0100
+++ b/src/Provers/blast.ML	Sun Mar 15 20:25:58 2009 +0100
@@ -1306,12 +1306,13 @@
 (** method setup **)
 
 val blast_method =
-  Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat))
-    (fn NONE => Data.cla_meth' blast_tac
-      | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));
+  Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
+  Method.sections Data.cla_modifiers >>
+  (fn (prems, NONE) => Data.cla_meth' blast_tac prems
+    | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems);
 
 val setup =
   setup_depth_limit #>
-  Method.add_methods [("blast", blast_method, "tableau prover")];
+  Method.setup @{binding blast} blast_method "tableau prover";
 
 end;
diff -r 5e2d9604a3d3 -r 9f168bdc468a src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sun Mar 15 20:19:14 2009 +0100
+++ b/src/Provers/clasimp.ML	Sun Mar 15 20:25:58 2009 +0100
@@ -296,28 +296,30 @@
 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;
-val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
 
+fun clasimp_method tac =
+  Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth tac);
 
-fun auto_args m =
-  Method.bang_sectioned_args' clasimp_modifiers
-    (Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat))) m;
+fun clasimp_method' tac =
+  Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);
 
-fun auto_meth NONE = clasimp_meth (CHANGED_PROP o auto_tac)
-  | auto_meth (SOME (m, n)) = clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n));
+val auto_method =
+  Args.bang_facts -- Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
+  Method.sections clasimp_modifiers >>
+  (fn (prems, NONE) => clasimp_meth (CHANGED_PROP o auto_tac) prems
+    | (prems, SOME (m, n)) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)) prems);
 
 
 (* theory setup *)
 
 val clasimp_setup =
- (Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
-  Method.add_methods
-   [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
-    ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
-    ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
-    ("force", clasimp_method' force_tac, "force"),
-    ("auto", auto_args auto_meth, "auto"),
-    ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]);
+  Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
+  Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp" #>
+  Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
+  Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
+  Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
+  Method.setup @{binding auto} auto_method "auto" #>
+  Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
+    "clarify simplified goal";
 
 end;
diff -r 5e2d9604a3d3 -r 9f168bdc468a src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Mar 15 20:19:14 2009 +0100
+++ b/src/Provers/classical.ML	Sun Mar 15 20:25:58 2009 +0100
@@ -149,8 +149,8 @@
   val cla_modifiers: Method.modifier parser list
   val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
-  val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
-  val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
+  val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
+  val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
   val setup: theory -> theory
 end;
 
@@ -1025,23 +1025,29 @@
 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;
-val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
+fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
+fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
 
 
 
 (** setup_methods **)
 
-val setup_methods = Method.add_methods
- [("default", Method.thms_ctxt_args default, "apply some intro/elim rule (potentially classical)"),
-  ("rule", Method.thms_ctxt_args rule, "apply some intro/elim rule (potentially classical)"),
-  ("contradiction", Method.no_args contradiction, "proof by contradiction"),
-  ("clarify", cla_method' (CHANGED_PROP oo clarify_tac), "repeatedly apply safe steps"),
-  ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
-  ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
-  ("best", cla_method' best_tac, "classical prover (best-first)"),
-  ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
-  ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
+val setup_methods =
+  Method.setup @{binding default} (Attrib.thms >> default)
+    "apply some intro/elim rule (potentially classical)" #>
+  Method.setup @{binding rule} (Attrib.thms >> rule)
+    "apply some intro/elim rule (potentially classical)" #>
+  Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
+    "proof by contradiction" #>
+  Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
+    "repeatedly apply safe steps" #>
+  Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
+  Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
+  Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
+  Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
+    "classical prover (iterative deepening)" #>
+  Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
+    "classical prover (apply safe rules)";
 
 
 
diff -r 5e2d9604a3d3 -r 9f168bdc468a src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Sun Mar 15 20:19:14 2009 +0100
+++ b/src/Tools/induct_tacs.ML	Sun Mar 15 20:25:58 2009 +0100
@@ -26,7 +26,7 @@
       error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
   in (u, U) end;
 
-fun gen_case_tac ctxt0 (s, opt_rule) i st =
+fun gen_case_tac ctxt0 s opt_rule i st =
   let
     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
     val rule =
@@ -46,8 +46,8 @@
   in res_inst_tac ctxt [(xi, s)] rule i st end
   handle THM _ => Seq.empty;
 
-fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
-fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
+fun case_tac ctxt s = gen_case_tac ctxt s NONE;
+fun case_rule_tac ctxt s rule = gen_case_tac ctxt s (SOME rule);
 
 
 (* induction *)
@@ -63,7 +63,7 @@
 
 in
 
-fun gen_induct_tac ctxt0 (varss, opt_rules) i st =
+fun gen_induct_tac ctxt0 varss opt_rules i st =
   let
     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
     val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
@@ -103,8 +103,8 @@
 
 end;
 
-fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE);
-fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt (args, SOME rules);
+fun induct_tac ctxt args = gen_induct_tac ctxt args NONE;
+fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt args (SOME rules);
 
 
 (* method syntax *)
@@ -122,11 +122,14 @@
 in
 
 val setup =
-  Method.add_methods
-   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name_source -- opt_rule) gen_case_tac,
-      "unstructured case analysis on types"),
-    ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
-      "unstructured induction on types")];
+  Method.setup @{binding case_tac}
+    (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >>
+      (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
+    "unstructured case analysis on types" #>
+  Method.setup @{binding induct_tac}
+    (Args.goal_spec -- varss -- opt_rules >>
+      (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
+    "unstructured induction on types";
 
 end;
 
diff -r 5e2d9604a3d3 -r 9f168bdc468a src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sun Mar 15 20:19:14 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Sun Mar 15 20:25:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Tools/induct_tacs.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
@@ -177,11 +176,14 @@
 (* theory setup *)
 
 val setup =
-  Method.add_methods
-    [("induct_tac", Method.goal_args_ctxt Args.name induct_tac,
-      "induct_tac emulation (dynamic instantiation!)"),
-     ("case_tac", Method.goal_args_ctxt Args.name exhaust_tac,
-      "datatype case_tac emulation (dynamic instantiation!)")];
+  Method.setup @{binding induct_tac}
+    (Args.goal_spec -- Scan.lift Args.name >>
+      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
+    "induct_tac emulation (dynamic instantiation!)" #>
+  Method.setup @{binding case_tac}
+   (Args.goal_spec -- Scan.lift Args.name >>
+      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
+    "datatype case_tac emulation (dynamic instantiation!)";
 
 
 (* outer syntax *)
diff -r 5e2d9604a3d3 -r 9f168bdc468a src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Sun Mar 15 20:19:14 2009 +0100
+++ b/src/ZF/Tools/typechk.ML	Sun Mar 15 20:25:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Tools/typechk.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
 
@@ -111,10 +110,10 @@
 (* concrete syntax *)
 
 val typecheck_meth =
-  Method.only_sectioned_args
+  Method.sections
     [Args.add -- Args.colon >> K (I, TC_add),
      Args.del -- Args.colon >> K (I, TC_del)]
-  (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
+  >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))));
 
 val _ =
   OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
@@ -126,7 +125,7 @@
 
 val setup =
   Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
-  Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
+  Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #>
   Simplifier.map_simpset (fn ss => ss setSolver type_solver);
 
 end;