src/HOL/Tools/lin_arith.ML

         @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
         @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
         @{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;
 
 val fast_nat_arith_simproc =