src/HOL/Euclidean_Division.thy
changeset 66813 351142796345
parent 66810 cc2b490f9dc4
child 66814 a24cde9588bb
     1.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -755,12 +755,8 @@
     1.4    val div_name = @{const_name divide};
     1.5    val mod_name = @{const_name modulo};
     1.6    val mk_binop = HOLogic.mk_binop;
     1.7 -  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
     1.8    val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
     1.9 -  fun mk_sum' [] = HOLogic.zero
    1.10 -    | mk_sum' [t] = t
    1.11 -    | mk_sum' (t :: ts) = mk_plus (t, mk_sum' ts);
    1.12 -  fun mk_sum _ = mk_sum';
    1.13 +  val mk_sum = Arith_Data.mk_sum;
    1.14    fun dest_sum tm =
    1.15      if HOLogic.is_zero tm then []
    1.16      else