# HG changeset patch
# User haftmann
# Date 1507494501 -7200
# Node ID 7163b780549daf0da8f7cd7a9660544431d8cb5e
# Parent  aa288270732af897e069526240d17c083f0a4c9f
adjusted implementation according to comment

diff -r aa288270732a -r 7163b780549d src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Tools/arith_data.ML	Sun Oct 08 22:28:21 2017 +0200
@@ -71,7 +71,7 @@
 
 (*this version ALWAYS includes a trailing zero*)
 fun long_mk_sum T [] = mk_number T 0
-  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
+  | long_mk_sum T (t :: ts) = mk_plus (t, long_mk_sum T ts);
 
 (*decompose additions AND subtractions as a sum*)
 fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) =