# 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.