src/HOL/Tools/lin_arith.ML

--- a/src/HOL/Tools/lin_arith.ML	Wed Nov 23 22:07:55 2011 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Wed Nov 23 22:59:39 2011 +0100
@@ -807,7 +807,7 @@
       addsimprocs [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}]
        (*abel_cancel helps it work in abstract algebraic domains*)
       addsimprocs Nat_Arith.nat_cancel_sums_add
-      addcongs [@{thm if_weak_cong}],
+      |> Simplifier.add_cong @{thm if_weak_cong},
     number_of = number_of}) #>
   add_discrete_type @{type_name nat};