src/ZF/IMP/Equiv.ML

--- a/src/ZF/IMP/Equiv.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/IMP/Equiv.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -120,7 +120,7 @@
 
 goal Equiv.thy
     "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
-by (fast_tac (!claset addIs [equalityI, C_subset RS subsetD]
+by (fast_tac (!claset addIs [C_subset RS subsetD]
 	              addEs [com2 RS bspec]
 		      addDs [com1]
 		      addss (!simpset)) 1);