--- a/src/Pure/tactic.ML Mon Jan 24 18:16:57 2005 +0100
+++ b/src/Pure/tactic.ML Mon Jan 24 18:18:28 2005 +0100
@@ -114,6 +114,7 @@
val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
int -> tactic
val lift_inst_rule' : thm * int * (indexname * string) list * thm -> thm
+ val eres_inst_tac' : (indexname * string) list -> thm -> int -> tactic
val res_inst_tac' : (indexname * string) list -> thm -> int -> tactic
end;
@@ -315,6 +316,9 @@
fun eres_inst_tac sinsts rule i =
compose_inst_tac sinsts (true, rule, nprems_of rule) i;
+fun eres_inst_tac' sinsts rule i =
+ compose_inst_tac' sinsts (true, rule, nprems_of rule) i;
+
(*For forw_inst_tac and dres_inst_tac. Preserve Var indexes of rl;
increment revcut_rl instead.*)
fun make_elim_preserve rl =