# HG changeset patch
# User berghofe
# Date 1106587108 -3600
# Node ID 02cc838b64cac4a059a724569fe1d54f22a46517
# Parent  95cb3eb74307e128c0c08dc8314a7666ff216e8c
Added variant of eres_inst_tac that operates on indexnames instead of strings.

diff -r 95cb3eb74307 -r 02cc838b64ca src/Pure/tactic.ML
--- 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 =