# HG changeset patch
# User nipkow
# Date 1008181199 -3600
# Node ID 32e67277a4b99b246969de0e198cc0c819f85855
# Parent  ed46612ad7ecec8b435b12bd8a9f30d782f71df7
tuned conversion from terms to "polynomials" for arith_tac: takes care
of "uminus" now.

diff -r ed46612ad7ec -r 32e67277a4b9 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Dec 12 18:05:44 2001 +0100
+++ b/src/HOL/arith_data.ML	Wed Dec 12 19:19:59 2001 +0100
@@ -267,6 +267,8 @@
 fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
         Const("Numeral.number_of",_)$n
         => demult(t,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
+      | Const("uminus",_)$(Const("Numeral.number_of",_)$n)
+        => demult(t,ratmul(m,rat_of_int(~(HOLogic.dest_binum n))))
       | Const("Suc",_) $ _
         => demult(t,ratmul(m,rat_of_int(number_of_Sucs s)))
       | Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
@@ -284,6 +286,7 @@
   | demult(t as Const("Numeral.number_of",_)$n,m) =
       ((None,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
        handle TERM _ => (Some t,m))
+  | demult(Const("uminus",_)$t, m) = demult(t,ratmul(m,rat_of_int(~1)))
   | demult(atom,m) = (Some atom,m)
 
 and atomult(mC,atom,t,m) = (case demult(t,m) of (None,m') => (Some atom,m')