# HG changeset patch
# User wenzelm
# Date 1198329025 -3600
# Node ID 6810d07f29dedf56e292ccf174b08b1132bf7cba
# Parent  1051ef9d87c4124dc36984b01afbebc5fb974671
tuned RandomWord interface;

diff -r 1051ef9d87c4 -r 6810d07f29de src/Tools/Metis/metis.ML
--- 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.                                                *)
diff -r 1051ef9d87c4 -r 6810d07f29de src/Tools/Metis/src/PortableIsabelle.sml
--- a/src/Tools/Metis/src/PortableIsabelle.sml	Sat Dec 22 14:10:24 2007 +0100
+++ b/src/Tools/Metis/src/PortableIsabelle.sml	Sat Dec 22 14:10:25 2007 +0100
@@ -33,12 +33,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;
+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
+end;
 
 (* ------------------------------------------------------------------------- *)
 (* Quotations a la Moscow ML.                                                *)