adjusted implementation according to comment
authorhaftmann
Sun Oct 08 22:28:21 2017 +0200 (19 months ago)
changeset 668127163b780549d
parent 66811 aa288270732a
child 66813 351142796345
adjusted implementation according to comment
src/HOL/Tools/arith_data.ML
     1.1 --- a/src/HOL/Tools/arith_data.ML	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Tools/arith_data.ML	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5  (*this version ALWAYS includes a trailing zero*)
     1.6  fun long_mk_sum T [] = mk_number T 0
     1.7 -  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
     1.8 +  | long_mk_sum T (t :: ts) = mk_plus (t, long_mk_sum T ts);
     1.9  
    1.10  (*decompose additions AND subtractions as a sum*)
    1.11  fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) =