# HG changeset patch
# User wenzelm
# Date 1464787049 -7200
# Node ID 13b67739af09cbc33922b2a81262daf2946704f7
# Parent  97b721666890a7512cec6f94e9f50410c1702268
clarified signature;

diff -r 97b721666890 -r 13b67739af09 src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Wed Jun 01 15:10:27 2016 +0200
+++ b/src/Pure/General/rat.ML	Wed Jun 01 15:17:29 2016 +0200
@@ -25,8 +25,8 @@
   val mult: rat -> rat -> rat
   val neg: rat -> rat
   val inv: rat -> rat
-  val round_down: rat -> rat
-  val round_up: rat -> rat
+  val floor: rat -> int
+  val ceil: rat -> int
 end;
 
 structure Rat : RAT =
@@ -91,12 +91,12 @@
   | EQUAL => raise DIVZERO
   | GREATER => Rat (q, p));
 
-fun round_down (Rat (p, q)) = Rat (p div q, 1);
+fun floor (Rat (p, q)) = p div q;
 
-fun round_up (Rat (p, q)) =
+fun ceil (Rat (p, q)) =
   (case Integer.div_mod p q of
-    (m, 0) => Rat (m, 1)
-  | (m, _) => Rat (m + 1, 1));
+    (m, 0) => m
+  | (m, _) => m);
 
 end;