# HG changeset patch
# User huffman
# Date 1362595483 28800
# Node ID abdcf1a7cabf2eeda954e282fc6acc268a098d78
# Parent  6b5250100db8243adc371e4e9a9282ead1515585
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)

diff -r 6b5250100db8 -r abdcf1a7cabf src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Wed Mar 06 16:56:21 2013 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Wed Mar 06 10:44:43 2013 -0800
@@ -499,8 +499,12 @@
           if u aconv t then (rev past @ terms)
           else find_first_t (t::past) u terms
 
+  fun dest_summing (Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
+        dest_summing (t, dest_summing (u, ts))
+    | dest_summing (t, ts) = t :: ts
+
   val mk_sum = Arith_Data.long_mk_sum
-  val dest_sum = Arith_Data.dest_sum
+  fun dest_sum t = dest_summing (t, [])
   val find_first = find_first_t []
   val trans_tac = Numeral_Simprocs.trans_tac
   val norm_ss = HOL_basic_ss addsimps