diff -r d945f05e75a2 -r 6e437e276ef5 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Dec 16 04:19:20 2004 +0100
+++ b/src/Provers/hypsubst.ML	Thu Dec 16 12:44:32 2004 +0100
@@ -18,8 +18,10 @@
 Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
 Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
 
+Goal "!!x a. [| x = f(b); g(a) = b |] ==> P(x)";
+
+by (bound_hyp_subst_tac 1);
 by (hyp_subst_tac 1);
-by (bound_hyp_subst_tac 1);
 
 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
 Goal "P(a) --> (EX y. a=y --> P(f(a)))";
@@ -55,7 +57,7 @@
   val vars_gen_hyp_subst_tac : bool -> int -> tactic
   val eq_var                 : bool -> bool -> term -> int * bool
   val inspect_pair           : bool -> bool -> term * term * typ -> bool
-  val mk_eqs                 : thm -> thm list
+  val mk_eqs                 : bool -> thm -> thm list
   val stac		     : thm -> int -> tactic
   val hypsubst_setup         : (theory -> theory) list
   end;
@@ -127,8 +129,8 @@
 
 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   No vars are allowed here, as simpsets are built from meta-assumptions*)
-fun mk_eqs th =
-    [ if inspect_pair false false (Data.dest_eq
+fun mk_eqs bnd th =
+    [ if inspect_pair bnd false (Data.dest_eq
                                    (Data.dest_Trueprop (#prop (rep_thm th))))
       then th RS Data.eq_reflection
       else symmetric(th RS Data.eq_reflection) (*reorient*) ]
@@ -137,13 +139,12 @@
 local open Simplifier
 in
 
-  val hyp_subst_ss = empty_ss setmksimps mk_eqs
-
-  (*Select a suitable equality assumption and substitute throughout the subgoal
-    Replaces only Bound variables if bnd is true*)
+  (*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 =
     let val tac = SUBGOAL (fn (Bi, i) =>
       let val (k, _) = eq_var bnd true Bi
+          val hyp_subst_ss = empty_ss setmksimps (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)