diff -r 56aa53caf333 -r 01cbbf33779b src/ZF/Integ/Int.ML
--- a/src/ZF/Integ/Int.ML	Mon May 21 14:52:04 2001 +0200
+++ b/src/ZF/Integ/Int.ML	Mon May 21 14:52:27 2001 +0200
@@ -77,7 +77,7 @@
 by Auto_tac;
 qed "int_of_type";
 
-AddIffs [int_of_type];
+Addsimps [int_of_type];
 AddTCs  [int_of_type];