diff -r fbc60cd02ae2 -r a657683e902a src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Wed Feb 20 14:52:34 2008 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Wed Feb 20 14:52:38 2008 +0100
@@ -810,7 +810,7 @@
         @{thm "not_one_less_zero"}]
       addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
        (*abel_cancel helps it work in abstract algebraic domains*)
-      addsimprocs nat_cancel_sums_add}) #>
+      addsimprocs ArithData.nat_cancel_sums_add}) #>
   arith_discrete "nat";
 
 val lin_arith_simproc = Fast_Arith.lin_arith_simproc;