--- a/src/Pure/General/random_word.ML Wed Dec 19 23:49:28 2007 +0100
+++ b/src/Pure/General/random_word.ML Thu Dec 20 00:19:40 2007 +0100
@@ -10,6 +10,7 @@
signature RANDOM_WORD =
sig
val range: int
+ val range_real: real
val next: unit -> word
val next_bit: unit -> bool
end;
@@ -21,6 +22,7 @@
val _ = Word.wordSize >= 30 orelse raise Fail ("Bad platform word size");
val range = 0x40000000;
+val range_real = 1073741824.0;
val mask = Word.fromInt (range - 1);
val max_bit = Word.fromInt (range div 2);
--- a/src/Tools/Metis/metis.ML Wed Dec 19 23:49:28 2007 +0100
+++ b/src/Tools/Metis/metis.ML Thu Dec 20 00:19:40 2007 +0100
@@ -198,9 +198,7 @@
val randomWord = RandomWord.next;
val randomBool = RandomWord.next_bit;
fun randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
-
-val normalizer = 1.0 / real RandomWord.range;
-fun randomReal () = real (Word.toInt (RandomWord.next ())) * normalizer;
+fun randomReal () = real (Word.toInt (RandomWord.next ())) / RandomWord.range_real;
end
--- a/src/Tools/Metis/src/PortableIsabelle.sml Wed Dec 19 23:49:28 2007 +0100
+++ b/src/Tools/Metis/src/PortableIsabelle.sml Thu Dec 20 00:19:40 2007 +0100
@@ -36,9 +36,7 @@
val randomWord = RandomWord.next;
val randomBool = RandomWord.next_bit;
fun randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
-
-val normalizer = 1.0 / real RandomWord.range;
-fun randomReal () = real (Word.toInt (RandomWord.next ())) * normalizer;
+fun randomReal () = real (Word.toInt (RandomWord.next ())) / RandomWord.range_real;
end