diff -r c583ca33076a -r da38571dd5bd src/Pure/General/rat.ML --- a/src/Pure/General/rat.ML Tue May 31 21:54:10 2016 +0200 +++ b/src/Pure/General/rat.ML Tue May 31 22:39:28 2016 +0200 @@ -32,18 +32,16 @@ structure Rat : RAT = struct +datatype rat = Rat of int * int; (*nominator, denominator (positive!)*) + fun common (p1, q1) (p2, q2) = - let - val m = Integer.lcm q1 q2; + let val m = PolyML.IntInf.lcm (q1, q2) in ((p1 * (m div q1), p2 * (m div q2)), m) end; -datatype rat = Rat of int * int; (*nominator, denominator (positive!)*) - exception DIVZERO; fun rat_of_quotient (p, q) = - let - val m = Integer.gcd (Int.abs p) q + let val m = PolyML.IntInf.gcd (p, q) in Rat (p div m, q div m) end handle Div => raise DIVZERO; fun quotient_of_rat (Rat r) = r;