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