# HG changeset patch
# User bulwahn
# Date 1352400935 -3600
# Node ID 4d17291eb19ca380ecf1c2d06c0a97d4cf5c7b9c
# Parent  c48b9b9f796da739cdc9af7a0d41b0bcef00b837
hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call

diff -r c48b9b9f796d -r 4d17291eb19c src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Nov 08 19:55:19 2012 +0100
+++ b/src/Provers/hypsubst.ML	Thu Nov 08 19:55:35 2012 +0100
@@ -48,6 +48,7 @@
 sig
   val bound_hyp_subst_tac    : int -> tactic
   val hyp_subst_tac          : int -> tactic
+  val hyp_subst_tac'         : simpset -> int -> tactic
   val blast_hyp_subst_tac    : bool -> int -> tactic
   val stac                   : thm -> int -> tactic
   val hypsubst_setup         : theory -> theory
@@ -126,12 +127,14 @@
 
   (*Select a suitable equality assumption; substitute throughout the subgoal
     If bnd is true, then it replaces Bound variables only. *)
-  fun gen_hyp_subst_tac bnd =
+  fun gen_hyp_subst_tac opt_ss bnd =
     let fun tac i st = SUBGOAL (fn (Bi, _) =>
       let
         val (k, _) = eq_var bnd true Bi
-        val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
-          |> Simplifier.set_mksimps (K (mk_eqs bnd))
+        val map_simpset = case opt_ss of
+          NONE => Simplifier.global_context (Thm.theory_of_thm st)
+        | SOME ss => Simplifier.inherit_context ss
+        val hyp_subst_ss = map_simpset empty_ss |> Simplifier.set_mksimps (K (mk_eqs bnd))
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
         etac thin_rl i, rotate_tac (~k) i]
       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
@@ -195,11 +198,14 @@
 
 (*Substitutes for Free or Bound variables*)
 val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
-        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
+        gen_hyp_subst_tac NONE false, vars_gen_hyp_subst_tac false];
+
+fun hyp_subst_tac' ss = FIRST' [ematch_tac [Data.thin_refl],
+        gen_hyp_subst_tac (SOME ss) false, vars_gen_hyp_subst_tac false];
 
 (*Substitutes for Bound variables only -- this is always safe*)
 val bound_hyp_subst_tac =
-    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
+    gen_hyp_subst_tac NONE true ORELSE' vars_gen_hyp_subst_tac true;
 
 
 (** Version for Blast_tac.  Hyps that are affected by the substitution are