diff -r e22d5a7f5f9f -r f02021cf7cec Nat.ML
--- a/Nat.ML	Wed Mar 15 10:44:26 1995 +0100
+++ b/Nat.ML	Fri Mar 17 15:48:55 1995 +0100
@@ -433,4 +433,4 @@
 by (simp_tac (nat_ss0 addsimps [le_eq_less_or_eq]) 1);
 qed "Suc_le_mono";
 
-val nat_ss = nat_ss0 addsimps [le_refl];
+val nat_ss = nat_ss0 addsimps [le_refl,Suc_le_mono];