avoid variant of mk_sum

--- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -755,12 +755,8 @@
   val div_name = @{const_name divide};
   val mod_name = @{const_name modulo};
   val mk_binop = HOLogic.mk_binop;
-  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
-  fun mk_sum' [] = HOLogic.zero
-    | mk_sum' [t] = t
-    | mk_sum' (t :: ts) = mk_plus (t, mk_sum' ts);
-  fun mk_sum _ = mk_sum';
+  val mk_sum = Arith_Data.mk_sum;
   fun dest_sum tm =
     if HOLogic.is_zero tm then []
     else