1.1 --- a/src/HOL/arith_data.ML	Thu Aug 20 16:37:18 1998 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Thu Aug 20 16:44:05 1998 +0200
     1.3 @@ -230,5 +230,5 @@
     1.4  by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
     1.5  				      Suc_diff_n]) 1);
     1.6  by (Clarify_tac 1);
     1.7 -by (asm_simp_tac (simpset() addsimps [less_imp_diff_is_0]) 1);
     1.8 +by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
     1.9  qed_spec_mp "diff_less_mono2";