src/Pure/library.ML
changeset 14618 068bb99f3ebd
parent 14472 cba7c0a3ffb3
child 14792 b7dac2fae5bb
--- a/src/Pure/library.ML	Sat Apr 17 16:24:36 2004 +0200
+++ b/src/Pure/library.ML	Sat Apr 17 17:08:53 2004 +0200
@@ -1145,7 +1145,7 @@
 
 exception RANDOM;
 
-fun rmod x y = x - y * real (Real.floor (x / y));
+fun rmod x y = x - y * Real.realFloor (x / y);
 
 local
   val a = 16807.0;