tuned RandomWord signature;

--- a/src/Pure/General/random_word.ML	Wed Dec 19 23:10:17 2007 +0100
+++ b/src/Pure/General/random_word.ML	Wed Dec 19 23:42:20 2007 +0100
@@ -9,7 +9,7 @@
 
 signature RANDOM_WORD =
 sig
-  val range: word
+  val range: int
   val next: unit -> word
   val next_bit: unit -> bool
 end;
@@ -18,12 +18,11 @@
 struct
 
 (*minimal length of unboxed words on all known platforms*)
-val bits = 30;
-val _ = Word.wordSize >= bits orelse raise Fail ("Bad platform word size");
+val _ = Word.wordSize >= 30 orelse raise Fail ("Bad platform word size");
 
-val range = 0wx40000000;
-val mask = range - 0w1;
-val max_bit = Word.>> (range, 0w1);
+val range = 0x40000000;
+val mask = Word.fromInt (range - 1);
+val max_bit = Word.fromInt (range div 2);
 
 (*multiplier according to Borosh and Niederreiter (for m = 2^30),
   cf. http://random.mat.sbg.ac.at/~charly/server/server.html*)

--- a/src/Tools/Metis/metis.ML	Wed Dec 19 23:10:17 2007 +0100
+++ b/src/Tools/Metis/metis.ML	Wed Dec 19 23:42:20 2007 +0100
@@ -199,9 +199,8 @@
 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;
+val normalizer = 1.0 / real RandomWord.range;
+fun randomReal () = real (Word.toInt (RandomWord.next ())) * normalizer;
 
 end
 

--- a/src/Tools/Metis/src/PortableIsabelle.sml	Wed Dec 19 23:10:17 2007 +0100
+++ b/src/Tools/Metis/src/PortableIsabelle.sml	Wed Dec 19 23:42:20 2007 +0100
@@ -37,9 +37,8 @@
 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;
+val normalizer = 1.0 / real RandomWord.range;
+fun randomReal () = real (Word.toInt (RandomWord.next ())) * normalizer;
 
 end