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.