--- 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];