# HG changeset patch
# User wenzelm
# Date 967487447 -7200
# Node ID c2f2f70bbb6018335feac7c2492a01533a0177da
# Parent  bf65780eed024c4c710cbd65412c7a4e670f9b59
'induct_tac' / 'case_tac': Method.goal_args';

diff -r bf65780eed02 -r c2f2f70bbb60 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Aug 28 20:29:56 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Aug 28 20:30:47 2000 +0200
@@ -231,16 +231,12 @@
 
 val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
 
-fun tactic_syntax args tac =
-  #2 oo Method.syntax (Args.goal_spec HEADGOAL -- (args -- opt_rule) >>
-    (fn (quant, x) => Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac x))));
-
 in
 
 val tactic_emulations =
- [("induct_tac", tactic_syntax varss gen_induct_tac,
+ [("induct_tac", Method.goal_args' (varss -- opt_rule) gen_induct_tac,
     "induct_tac emulation (dynamic instantiation!)"),
-  ("case_tac", tactic_syntax (Scan.lift Args.name) gen_case_tac,
+  ("case_tac", Method.goal_args' (Scan.lift Args.name -- opt_rule) gen_case_tac,
     "case_tac emulation (dynamic instantiation!)")];
 
 end;