# HG changeset patch
# User wenzelm
# Date 1464813351 -7200
# Node ID 2cddda300fc787fb47fe1b37a3b7431baddab5e2
# Parent  20758395785a4fe3c33da045856369b4384e56a0
proper ceil operation;

diff -r 20758395785a -r 2cddda300fc7 src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Wed Jun 01 21:31:08 2016 +0200
+++ b/src/Pure/General/rat.ML	Wed Jun 01 22:35:51 2016 +0200
@@ -89,7 +89,7 @@
 fun ceil (Rat (p, q)) =
   (case Integer.div_mod p q of
     (m, 0) => m
-  | (m, _) => m);
+  | (m, _) => m + 1);
 
 end;