# HG changeset patch
# User wenzelm
# Date 1464809468 -7200
# Node ID 20758395785a4fe3c33da045856369b4384e56a0
# Parent  240d77628775ec9184dd473856dfc4793d7efd03
tuned;

diff -r 240d77628775 -r 20758395785a src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Wed Jun 01 21:26:39 2016 +0200
+++ b/src/Pure/General/rat.ML	Wed Jun 01 21:31:08 2016 +0200
@@ -31,6 +31,8 @@
 
 datatype rat = Rat of int * int;  (*numerator, positive (!) denominator*)
 
+fun of_int i = Rat (i, 1);
+
 fun common (p1, q1) (p2, q2) =
   let val m = PolyML.IntInf.lcm (q1, q2)
   in ((p1 * (m div q1), p2 * (m div q2)), m) end;
@@ -44,8 +46,6 @@
 
 fun dest (Rat r) = r;
 
-fun of_int i = Rat (i, 1);
-
 fun string_of_rat (Rat (p, 1)) = string_of_int p
   | string_of_rat (Rat (p, q)) = string_of_int p ^ "/" ^ string_of_int q;
 
@@ -70,8 +70,8 @@
 
 fun abs (r as Rat (p, q)) = if p < 0 then Rat (~ p, q) else r;
 
-fun add (Rat (p1, q1)) (Rat (p2, q2)) =
-  let val ((m1, m2), n) = common (p1, q1) (p2, q2)
+fun add (Rat r1) (Rat r2) =
+  let val ((m1, m2), n) = common r1 r2
   in make (m1 + m2, n) end;
 
 fun mult (Rat (p1, q1)) (Rat (p2, q2)) = make (p1 * p2, q1 * q2);