# HG changeset patch
# User wenzelm
# Date 1007427645 -3600
# Node ID e4be26df707a98db9e491a3481a1a47c5b5c5245
# Parent  92c48cc45e78d635725b72092cb62b715050d87a
no need for hyp_subst_tac' (!?);

diff -r 92c48cc45e78 -r e4be26df707a src/FOL/hypsubstdata.ML
--- a/src/FOL/hypsubstdata.ML	Tue Dec 04 02:00:14 2001 +0100
+++ b/src/FOL/hypsubstdata.ML	Tue Dec 04 02:00:45 2001 +0100
@@ -14,12 +14,8 @@
   val subst = subst
   val sym = sym
   val thin_refl = prove_goal (the_context ())
-		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
+                  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
   end;
 
 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;