src/ZF/AC/AC16_WO4.ML

 Addsimps [knat];  AddSIs [knat];
 
 AddSIs [Infinite];   (*if notI is removed!*)
 AddSEs [Infinite RS notE];
 
-AddEs [IntI RS (disjoint RS equals0E)];
+AddEs [[disjoint, IntI] MRS (equals0D RS notE)];
 
 (*use k = succ(l) *)
 val includes_l = simplify (FOL_ss addsimps [k_def]) includes;
 val all_ex_l = simplify (FOL_ss addsimps [k_def]) all_ex;