diff -r 7237c6497cb1 -r 5d1436d1c268 src/FOL/hypsubstdata.ML
--- a/src/FOL/hypsubstdata.ML	Mon Dec 03 20:59:57 2001 +0100
+++ b/src/FOL/hypsubstdata.ML	Mon Dec 03 21:01:11 2001 +0100
@@ -19,3 +19,7 @@
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;
+
+fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
+  Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("o", []) | _ => false)
+    (Library.nth_elem (i - 1, Thm.prems_of thm)) then hyp_subst_tac i thm else no_tac thm;