# HG changeset patch
# User oheimb
# Date 879357530 -3600
# Node ID f60e3d2c81d3c719ec5ee5079cce1f671c5de010
# Parent  d7573d6d051307d20250abb9c1bffecc3afa8d40
added thin_refl to hyp_subst_tac

diff -r d7573d6d0513 -r f60e3d2c81d3 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
+++ b/src/FOL/ROOT.ML	Wed Nov 12 18:58:50 1997 +0100
@@ -34,6 +34,8 @@
   val rev_mp = rev_mp
   val subst = subst
   val sym = sym
+  val thin_refl = prove_goal IFOL.thy 
+		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
   end;
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
diff -r d7573d6d0513 -r f60e3d2c81d3 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
+++ b/src/FOLP/ROOT.ML	Wed Nov 12 18:58:50 1997 +0100
@@ -39,6 +39,8 @@
   val rev_mp = rev_mp
   val subst = subst
   val sym = sym
+  val thin_refl = prove_goal IFOLP.thy 
+		  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
   end;
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
diff -r d7573d6d0513 -r f60e3d2c81d3 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Wed Nov 12 16:28:53 1997 +0100
+++ b/src/HOL/cladata.ML	Wed Nov 12 18:58:50 1997 +0100
@@ -21,6 +21,8 @@
   val rev_mp = rev_mp
   val subst = subst
   val sym = sym
+  val thin_refl = prove_goal HOL.thy 
+		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
   end;
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
diff -r d7573d6d0513 -r f60e3d2c81d3 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Wed Nov 12 16:28:53 1997 +0100
+++ b/src/Provers/hypsubst.ML	Wed Nov 12 18:58:50 1997 +0100
@@ -3,8 +3,9 @@
     Authors: 	Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     Copyright   1995  University of Cambridge
 
-Tactic to substitute using the assumption x=t in the rest of the subgoal,
-and to delete that assumption.  Original version due to Martin Coen.
+Tactic to substitute using (at least) the assumption x=t in the rest of the 
+subgoal, and to delete (at least) that assumption. 
+Original version due to Martin Coen.
 
 This version uses the simplifier, and requires it to be already present.
 
@@ -31,7 +32,8 @@
   val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
   val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
   val sym	       : thm		   (* a=b ==> b=a *)
-  end;
+  val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
+end;
 
 
 signature HYPSUBST =
@@ -174,8 +176,8 @@
       handle THM _ => no_tac | EQ_VAR => no_tac);
 
 (*Substitutes for Free or Bound variables*)
-val hyp_subst_tac = 
-    gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false;
+val hyp_subst_tac = FIRST' [ematch_tac [thin_refl],
+        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
 
 (*Substitutes for Bound variables only -- this is always safe*)
 val bound_hyp_subst_tac =