src/HOL/Tools/datatype_package.ML
changeset 9704 c2f2f70bbb60
parent 9386 8800603d99f6
child 9714 79db0e5b7824
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Aug 28 20:29:56 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Aug 28 20:30:47 2000 +0200
     1.3 @@ -231,16 +231,12 @@
     1.4  
     1.5  val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
     1.6  
     1.7 -fun tactic_syntax args tac =
     1.8 -  #2 oo Method.syntax (Args.goal_spec HEADGOAL -- (args -- opt_rule) >>
     1.9 -    (fn (quant, x) => Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac x))));
    1.10 -
    1.11  in
    1.12  
    1.13  val tactic_emulations =
    1.14 - [("induct_tac", tactic_syntax varss gen_induct_tac,
    1.15 + [("induct_tac", Method.goal_args' (varss -- opt_rule) gen_induct_tac,
    1.16      "induct_tac emulation (dynamic instantiation!)"),
    1.17 -  ("case_tac", tactic_syntax (Scan.lift Args.name) gen_case_tac,
    1.18 +  ("case_tac", Method.goal_args' (Scan.lift Args.name -- opt_rule) gen_case_tac,
    1.19      "case_tac emulation (dynamic instantiation!)")];
    1.20  
    1.21  end;