--- a/src/Tools/Metis/metis.ML Sat Dec 22 14:10:24 2007 +0100
+++ b/src/Tools/Metis/metis.ML Sat Dec 22 14:10:25 2007 +0100
@@ -100,12 +100,12 @@
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
-val randomWord = RandomWord.next;
-val randomBool = RandomWord.next_bit;
-fun randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
-fun randomReal () = real (Word.toInt (RandomWord.next ())) / RandomWord.range_real;
-
-end
+val randomWord = RandomWord.next_word;
+val randomBool = RandomWord.next_bool;
+fun randomInt n = RandomWord.next_int 0 (n - 1);
+val randomReal = RandomWord.next_real;
+
+end;
(* ------------------------------------------------------------------------- *)
(* Quotations a la Moscow ML. *)