Added variant of eres_inst_tac that operates on indexnames instead of strings.

--- 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 =