# HG changeset patch
# User wenzelm
# Date 1198101976 -3600
# Node ID 7a5dcfa5bbe2793e9df77a8f2b071c60f3353f05
# Parent  3d1d281b247126badb937c5d8a9e9683409f4781
updated;

diff -r 3d1d281b2471 -r 7a5dcfa5bbe2 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Wed Dec 19 23:06:14 2007 +0100
+++ b/src/Tools/Metis/metis.ML	Wed Dec 19 23:06:16 2007 +0100
@@ -195,27 +195,13 @@
 (* Generating random values.                                                 *)
 (* ------------------------------------------------------------------------- *)
 
-(* ------------------------------------------------------------------------- *)
-(* Generating random values.                                                 *)
-(* ------------------------------------------------------------------------- *)
-
-local
-  val gen = Random.newgenseed 1.0;
-in
-  fun randomInt max = Random.range (0,max) gen;
-
-  fun randomReal () = Random.random gen;
-end;
-
-fun randomBool () = randomInt 2 = 0;
-
-fun randomWord () =
-    let
-      val h = Word.fromInt (randomInt 65536)
-      and l = Word.fromInt (randomInt 65536)
-    in
-      Word.orb (Word.<< (h,0w16), l)
-    end;
+val randomWord = RandomWord.next;
+val randomBool = RandomWord.next_bit;
+fun randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
+
+val real_word = real o Word.toInt;
+val normalizer = 1.0 / real_word RandomWord.range;
+fun randomReal () = real_word (RandomWord.next ()) * normalizer;
 
 end