diff -r 6244be18fa55 -r 68c6159440f1 src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/Nat.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -74,6 +74,8 @@
 by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
 qed "nat_into_Ord";
 
+Addsimps [nat_into_Ord];
+
 (* i: nat ==> 0 le i; same thing as 0<succ(i)  *)
 bind_thm ("nat_0_le", nat_into_Ord RS Ord_0_le);