Now Collect_mem_eq is a default simprule (how could it have ever been omitted?

--- a/src/HOL/Set.ML	Tue Jul 01 10:34:30 1997 +0200
+++ b/src/HOL/Set.ML	Tue Jul 01 10:37:03 1997 +0200
@@ -10,7 +10,8 @@
 
 section "Relating predicates and sets";
 
-AddIffs [mem_Collect_eq];
+Addsimps [Collect_mem_eq];
+AddIffs  [mem_Collect_eq];
 
 goal Set.thy "!!a. P(a) ==> a : {x.P(x)}";
 by (Asm_simp_tac 1);