# HG changeset patch
# User nipkow
# Date 1074051676 -3600
# Node ID 9e3ce012f8430174b4a90b85ae61426e1c0135a5
# Parent  67e2e96bfe361840fb2e527e2c300c3340aa4aa7
fixed old bugs in "decomp" (conversion from term to lin.arith. format).
updated instantiation of real lin.arith.

diff -r 67e2e96bfe36 -r 9e3ce012f843 src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Wed Jan 14 00:13:04 2004 +0100
+++ b/src/HOL/Real/real_arith.ML	Wed Jan 14 04:41:16 2004 +0100
@@ -271,7 +271,7 @@
          real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, real_of_nat_mult,
          real_of_int_zero, real_of_one, real_of_int_add RS sym,
          real_of_int_minus RS sym, real_of_int_diff RS sym,
-         real_of_int_mult RS sym];
+         real_of_int_mult RS sym, real_number_of];
 
 val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,
                     real_of_int_inject RS iffD2];
diff -r 67e2e96bfe36 -r 9e3ce012f843 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Jan 14 00:13:04 2004 +0100
+++ b/src/HOL/arith_data.ML	Wed Jan 14 04:41:16 2004 +0100
@@ -283,6 +283,8 @@
       (let val den = HOLogic.dest_binum dent
        in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_int den))) end
        handle TERM _ => (Some atom,m))
+  | demult(Const("0",_),m) = (None, rat_of_int 0)
+  | demult(Const("1",_),m) = (None, m)
   | demult(t as Const("Numeral.number_of",_)$n,m) =
       ((None,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
        handle TERM _ => (Some t,m))
@@ -312,7 +314,7 @@
        | (Some u,m') => add_atom(u,m',pi))
   | poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) =
       (case demult inj_consts (t,m) of
-         (None,m') => (p,ratadd(i,m))
+         (None,m') => (p,ratadd(i,m'))
        | (Some u,m') => add_atom(u,m',pi))
   | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) =
       ((p,ratadd(i,ratmul(m,rat_of_int(HOLogic.dest_binum t))))