subset_empty is no longer a simprule

--- a/src/HOL/equalities.ML	Fri Jun 16 13:16:07 2000 +0200
+++ b/src/HOL/equalities.ML	Fri Jun 16 13:18:55 2000 +0200
@@ -18,10 +18,11 @@
 qed "Collect_const";
 Addsimps [Collect_const];
 
+(*If added as a simprule it can cause looping when equalityE is also present:
+  A={} goes to {}<=A and A<={} and then back to A={} !*)
 Goal "(A <= {}) = (A = {})";
 by (Blast_tac 1);
 qed "subset_empty";
-Addsimps [subset_empty];
 
 Goalw [psubset_def] "~ (A < {})";
 by (Blast_tac 1);