author | nipkow |
Mon, 08 Aug 2005 12:15:03 +0200 | |
changeset 17032 | 3e41d98bf6d4 |
parent 17031 | ffa73448025e |
child 17033 | f4c1ce91aa3c |
--- a/src/Pure/library.ML Mon Aug 08 09:29:16 2005 +0200 +++ b/src/Pure/library.ML Mon Aug 08 12:15:03 2005 +0200 @@ -1262,7 +1262,7 @@ in if a then p < r else r < p end fun ratadd(Rat(a,p,q),Rat(b,r,s)) = - let val (p,q,den) = ratcommon(p,q,r,s) + let val (p,r,den) = ratcommon(p,q,r,s) val num = (if a then p else ~p) + (if b then r else ~r) in ratnorm(true,num,den) end;