src/ZF/ex/Enum.ML

   val monos = [];
   val type_intrs = data_typechecks
   val type_elims = []);
 
 goal Enum.thy "~ con59=con60";
-by (SIMP_TAC (ZF_ss addrews Enum.free_iffs) 1);  (*2.3 secs*)
+by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);  (*2.3 secs*)
 result();