# HG changeset patch
# User haftmann
# Date 1507494501 -7200
# Node ID aa288270732af897e069526240d17c083f0a4c9f
# Parent  cc2b490f9dc4496a1414d0c75bfac7fb43e6b491
dropped duplicates

diff -r cc2b490f9dc4 -r aa288270732a src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sun Oct 08 22:28:21 2017 +0200
@@ -41,17 +41,9 @@
          handle TERM _ => find_first_numeral (t::past) terms)
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
-val zero = mk_number 0;
-val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
+val mk_sum = Arith_Data.mk_sum HOLogic.natT;
 
-(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
-fun mk_sum []        = zero
-  | mk_sum [t,u]     = mk_plus (t, u)
-  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-(*this version ALWAYS includes a trailing zero*)
-fun long_mk_sum []        = HOLogic.zero
-  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+val long_mk_sum = Arith_Data.long_mk_sum HOLogic.natT;
 
 val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;