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