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;