# HG changeset patch
# User wenzelm
# Date 955546819 -7200
# Node ID 5893f2952e4fb0f6684db465d5771c817c23d71d
# Parent  05b6e5bcab669f050e204d6ef887cbb278468a21
fixed 'induct_tac' syntax;

diff -r 05b6e5bcab66 -r 5893f2952e4f src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Apr 10 23:38:02 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 12 15:40:19 2000 +0200
@@ -213,16 +213,17 @@
 
 local
 
-val rule_spec = Scan.option (Scan.lift (Args.$$$ "rule" -- Args.$$$ ":") |-- Attrib.local_thm);
+val rule_spec = Args.$$$ "rule" -- Args.$$$ ":";
+val opt_rule = Scan.option (Scan.lift rule_spec |-- Attrib.local_thm);
 
 fun tactic_syntax args tac =
-  #2 oo Method.syntax (Args.goal_spec HEADGOAL -- (Scan.lift args -- rule_spec) >>
+  #2 oo Method.syntax (Args.goal_spec HEADGOAL -- (Scan.lift 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 (Scan.repeat1 Args.name) gen_induct_tac,
+ [("induct_tac", tactic_syntax (Scan.repeat1 (Scan.unless rule_spec Args.name)) gen_induct_tac,
     "induct_tac emulation (dynamic instantiation!)"),
   ("case_tac", tactic_syntax Args.name gen_case_tac,
     "case_tac emulation (dynamic instantiation!)")];