diff -r 1fbbc10d475b -r d95f3df451e5 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Oct 04 15:10:44 2006 +0200
+++ b/src/HOL/arith_data.ML	Wed Oct 04 18:41:14 2006 +0200
@@ -364,9 +364,11 @@
         (case demult inj_consts (all, m) of
            (NONE,   m') => (p, Rat.add (i, m'))
          | (SOME u, m') => add_atom u m' pi)
-    | poly (all as Const ("Numeral.number_of", _) $ t, m, pi as (p, i)) =
-        ((p, Rat.add (i, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum t))))
-         handle TERM _ => add_atom all m pi)
+    | poly (all as Const ("Numeral.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
+        (let val k = HOLogic.dest_binum t
+            val k2 = if k < 0 andalso T = HOLogic.natT then 0 else k
+        in (p, Rat.add (i, Rat.mult (m, Rat.rat_of_intinf k2))) end
+        handle TERM _ => add_atom all m pi)
     | poly (all as Const f $ x, m, pi) =
         if f mem inj_consts then poly (x, m, pi) else add_atom all m pi
     | poly (all, m, pi) =