src/HOL/Tools/datatype_package.ML
changeset 8686 5893f2952e4f
parent 8672 1f51c411da5a
child 8689 a2e82eed6454
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Apr 10 23:38:02 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 12 15:40:19 2000 +0200
     1.3 @@ -213,16 +213,17 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val rule_spec = Scan.option (Scan.lift (Args.$$$ "rule" -- Args.$$$ ":") |-- Attrib.local_thm);
     1.8 +val rule_spec = Args.$$$ "rule" -- Args.$$$ ":";
     1.9 +val opt_rule = Scan.option (Scan.lift rule_spec |-- Attrib.local_thm);
    1.10  
    1.11  fun tactic_syntax args tac =
    1.12 -  #2 oo Method.syntax (Args.goal_spec HEADGOAL -- (Scan.lift args -- rule_spec) >>
    1.13 +  #2 oo Method.syntax (Args.goal_spec HEADGOAL -- (Scan.lift args -- opt_rule) >>
    1.14      (fn (quant, x) => Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac x))));
    1.15  
    1.16  in
    1.17  
    1.18  val tactic_emulations =
    1.19 - [("induct_tac", tactic_syntax (Scan.repeat1 Args.name) gen_induct_tac,
    1.20 + [("induct_tac", tactic_syntax (Scan.repeat1 (Scan.unless rule_spec Args.name)) gen_induct_tac,
    1.21      "induct_tac emulation (dynamic instantiation!)"),
    1.22    ("case_tac", tactic_syntax Args.name gen_case_tac,
    1.23      "case_tac emulation (dynamic instantiation!)")];