1.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Jul 19 20:23:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Jul 19 20:23:52 2010 +0200
     1.3 @@ -818,7 +818,7 @@
     1.4          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
     1.5          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
     1.6          @{thm "not_one_less_zero"}]
     1.7 -      addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv]
     1.8 +      addsimprocs [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}]
     1.9         (*abel_cancel helps it work in abstract algebraic domains*)
    1.10        addsimprocs Nat_Arith.nat_cancel_sums_add
    1.11        addcongs [@{thm if_weak_cong}],