diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/enum.ML
--- a/src/ZF/ex/enum.ML	Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/enum.ML	Fri Sep 17 16:52:10 1993 +0200
@@ -28,6 +28,6 @@
   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();