# HG changeset patch
# User haftmann
# Date 1507494502 -7200
# Node ID 3511427963453aa7d3ef72c8eda9d47a04bf8103
# Parent  7163b780549daf0da8f7cd7a9660544431d8cb5e
avoid variant of mk_sum

diff -r 7163b780549d -r 351142796345 src/HOL/Euclidean_Division.thy
--- 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