src/Pure/library.ML
 changeset 2303 84ed9e0d7c50 parent 2271 7c4744ed8fc3 child 2317 672015b535d7
```     1.1 --- a/src/Pure/library.ML	Mon Dec 02 18:24:38 1996 +0100
1.2 +++ b/src/Pure/library.ML	Tue Dec 03 11:20:43 1996 +0100
1.3 @@ -889,12 +889,10 @@
1.4        in (x, zs) :: map step qs end;
1.5
1.6
1.7 -(** Recommended by Stephen K. Park and Keith W. Miller,
1.8 -      Random number generators: good ones are hard to find,
1.9 -      CACM 31 (1988), 1192-1201.
1.10 -    Real number version for systems with 46-bit mantissae
1.11 -    Computes  (a*seed) mod m ;  should be applied to integers only! **)
1.12 -local val a = 16807.0  and  m = 2147483647.0  (* 2^31 - 1 *)
1.13 +(** Simple random number generator; not guaranteed to be good, because modulus
1.14 +    has been reduced from 2^31-1 to 2^29-1 to prevent integer overflows
1.15 +**)
1.16 +local val a = 16807.0  and  m = 536870911.0  (* 2^29 - 1 *)
1.17  in  fun nextrandom seed =
1.18            let val t = a*seed
1.19            in  t - m * real(floor(t/m))  end
1.20 @@ -919,10 +917,9 @@
1.21            else  (*i=63*)    "'"
1.22    in  implode (map char (radixpand (64,n)))  end;
1.23
1.24 -(*Randomly generated identifiers with given prefix; MUST start with a letter
1.25 -    [division by two avoids overflow for ML systems whose maxint is 2^30 - 1 *)
1.26 +(*Randomly generated identifiers with given prefix; MUST start with a letter*)
1.27  fun gensym pre = pre ^
1.28 -                 (#1(newid (floor (!seedr/2.0)),
1.29 +                 (#1(newid (floor (!seedr)),
1.30                       seedr := nextrandom (!seedr)))
1.31
1.32  (*Increment a list of letters like a reversed base 26 number.
```