1.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Aug 28 22:08:02 2008 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 28 22:08:11 2008 +0200
     1.3 @@ -803,8 +803,8 @@
     1.4      neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
     1.5      simpset = HOL_basic_ss
     1.6        addsimps
     1.7 -       [@{thm "monoid_add_class.zero_plus.add_0_left"},
     1.8 -        @{thm "monoid_add_class.zero_plus.add_0_right"},
     1.9 +       [@{thm "monoid_add_class.add_0_left"},
    1.10 +        @{thm "monoid_add_class.add_0_right"},
    1.11          @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
    1.12          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
    1.13          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},