# HG changeset patch
# User paulson
# Date 843656593 -7200
# Node ID 9acc10ac1e1de3685756adbfb538f99b608ba98a
# Parent  909153d8318f1fea8998dbea0f5e813ec29867f3
Prevention of Overflow exception (for SML/NJ) in gensym

diff -r 909153d8318f -r 9acc10ac1e1d src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Sep 25 11:14:18 1996 +0200
+++ b/src/Pure/library.ML	Wed Sep 25 15:03:13 1996 +0200
@@ -910,7 +910,7 @@
       CACM 31 (1988), 1192-1201. 
     Real number version for systems with 46-bit mantissae
     Computes  (a*seed) mod m ;  should be applied to integers only! **)
-local val a = 16807.0  and  m = 2147483647.0
+local val a = 16807.0  and  m = 2147483647.0  (* 2^31 - 1 *)
 in  fun nextrandom seed =
           let val t = a*seed
           in  t - m * real(floor(t/m))  end
@@ -935,9 +935,11 @@
           else  (*i=63*)    "'"
   in  implode (map char (radixpand (64,n)))  end;
 
-(*Randomly generated identifiers with given prefix; MUST start with a letter*)
+(*Randomly generated identifiers with given prefix; MUST start with a letter
+    [division by two avoids overflow for ML systems whose maxint is 2^30 - 1 *)
 fun gensym pre = pre ^ 
-                 (#1(newid (floor (!seedr)), seedr := nextrandom (!seedr)))
+                 (#1(newid (floor (!seedr/2.0)), 
+		     seedr := nextrandom (!seedr)))
 
 (*Increment a list of letters like a reversed base 26 number.
   If head is "z", bumps chars in tail.