author nipkow Fri, 13 May 2005 19:55:09 +0200 changeset 15958 b4ea8bf8e2f7 parent 15957 f2a0a80d8233 child 15959 366d39e95d3c
-(n::nat) is now regarded as atomic
 src/HOL/arith_data.ML file | annotate | diff | comparison | revisions
```--- 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)))```