src/Pure/tactic.ML
changeset 15464 02cc838b64ca
parent 15453 6318e634e6cc
child 15531 08c8dad8e399
     1.1 --- a/src/Pure/tactic.ML	Mon Jan 24 18:16:57 2005 +0100
     1.2 +++ b/src/Pure/tactic.ML	Mon Jan 24 18:18:28 2005 +0100
     1.3 @@ -114,6 +114,7 @@
     1.4    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
     1.5                            int -> tactic
     1.6    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
     1.7 +  val eres_inst_tac'    : (indexname * string) list -> thm -> int -> tactic
     1.8    val res_inst_tac'     : (indexname * string) list -> thm -> int -> tactic
     1.9  end;
    1.10  
    1.11 @@ -315,6 +316,9 @@
    1.12  fun eres_inst_tac sinsts rule i =
    1.13      compose_inst_tac sinsts (true, rule, nprems_of rule) i;
    1.14  
    1.15 +fun eres_inst_tac' sinsts rule i =
    1.16 +    compose_inst_tac' sinsts (true, rule, nprems_of rule) i;
    1.17 +
    1.18  (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
    1.19    increment revcut_rl instead.*)
    1.20  fun make_elim_preserve rl =