diff -r cc2340c338f0 -r 6218522253e7 src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Mon Feb 28 10:49:08 2000 +0100
+++ b/src/HOL/UNITY/UNITY.ML	Mon Feb 28 10:49:42 2000 +0100
@@ -10,6 +10,9 @@
 
 set proof_timing;
 
+(*Perhaps equalities.ML shouldn't add this in the first place!*)
+Delsimps [image_Collect];
+
 
 (*** General lemmas ***)