# HG changeset patch
# User wenzelm
# Date 1198106380 -3600
# Node ID 5ae1dc2bb5ea3fc1c00afb5cd27e09f3265b8af0
# Parent  71e0a5cb28855f3997001eb2a1faa9456d1d31d4
Random.range_real makes SML/NJ happy;

diff -r 71e0a5cb2885 -r 5ae1dc2bb5ea src/Pure/General/random_word.ML
--- 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);
 
diff -r 71e0a5cb2885 -r 5ae1dc2bb5ea src/Tools/Metis/metis.ML
--- 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
 
diff -r 71e0a5cb2885 -r 5ae1dc2bb5ea src/Tools/Metis/src/PortableIsabelle.sml
--- 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