maintain invariant for exported operation;
authorwenzelm
Tue, 31 May 2016 23:06:03 +0200
changeset 63200 6eccfe9f5ef1
parent 63199 da38571dd5bd
child 63201 f151704c08e4
maintain invariant for exported operation;
src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Tue May 31 22:39:28 2016 +0200
+++ b/src/Pure/General/rat.ML	Tue May 31 23:06:03 2016 +0200
@@ -41,8 +41,10 @@
 exception DIVZERO;
 
 fun rat_of_quotient (p, q) =
-  let val m = PolyML.IntInf.gcd (p, q)
-  in Rat (p div m, q div m) end handle Div => raise DIVZERO;
+  let
+    val m = PolyML.IntInf.gcd (p, q);
+    val (p', q') = (p div m, q div m) handle Div => raise DIVZERO;
+  in Rat (if q' < 0 then (~ p', ~ q') else (p', q')) end
 
 fun quotient_of_rat (Rat r) = r;