# HG changeset patch
# User wenzelm
# Date 1198104140 -3600
# Node ID a51430528fe0e64015ef0a11fffcd2df9ae001a9
# Parent  75d5d23a5c208eaf5339b7e24aa1c56d137d5dad
tuned RandomWord signature;

diff -r 75d5d23a5c20 -r a51430528fe0 src/Pure/General/random_word.ML
--- 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*)
diff -r 75d5d23a5c20 -r a51430528fe0 src/Tools/Metis/metis.ML
--- 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
 
diff -r 75d5d23a5c20 -r a51430528fe0 src/Tools/Metis/src/PortableIsabelle.sml
--- 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