# HG changeset patch
# User nipkow
# Date 1116006909 -7200
# Node ID b4ea8bf8e2f7de23b9ed929f4fc41d89d6284825
# Parent  f2a0a80d82334be38b957f665bad582021b15ac8
-(n::nat) is now regarded as atomic

diff -r f2a0a80d8233 -r b4ea8bf8e2f7 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri May 13 17:19:04 2005 +0200
+++ b/src/HOL/arith_data.ML	Fri May 13 19:55:09 2005 +0200
@@ -301,9 +301,9 @@
 (* Turn term into list of summand * multiplicity plus a constant *)
 fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
   | poly(all as Const("op -",T) $ s $ t, m, pi) =
-      if nT T then add_atom(all,m,pi)
-      else poly(s,m,poly(t,ratneg m,pi))
-  | poly(Const("uminus",_) $ t, m, pi) = poly(t,ratneg m,pi)
+      if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,ratneg m,pi))
+  | poly(all as Const("uminus",T) $ t, m, pi) =
+      if nT T then add_atom(all,m,pi) else poly(t,ratneg m,pi)
   | poly(Const("0",_), _, pi) = pi
   | poly(Const("1",_), m, (p,i)) = (p,ratadd(i,m))
   | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))