src/HOL/Library/Extended_Nat.thy
changeset 51366 abdcf1a7cabf
parent 51301 6822aa82aafa
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Wed Mar 06 16:56:21 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Mar 06 10:44:43 2013 -0800
     1.3 @@ -499,8 +499,12 @@
     1.4            if u aconv t then (rev past @ terms)
     1.5            else find_first_t (t::past) u terms
     1.6  
     1.7 +  fun dest_summing (Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
     1.8 +        dest_summing (t, dest_summing (u, ts))
     1.9 +    | dest_summing (t, ts) = t :: ts
    1.10 +
    1.11    val mk_sum = Arith_Data.long_mk_sum
    1.12 -  val dest_sum = Arith_Data.dest_sum
    1.13 +  fun dest_sum t = dest_summing (t, [])
    1.14    val find_first = find_first_t []
    1.15    val trans_tac = Numeral_Simprocs.trans_tac
    1.16    val norm_ss = HOL_basic_ss addsimps