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) =