--- 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!)")];