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 ArithData.nat_cancel_sums_add}) #>
+      addsimprocs Nat_Arith.nat_cancel_sums_add}) #>
   arith_discrete "nat";
 
 fun add_arith_facts ss =
   add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) ss;