--- a/src/Pure/library.ML Tue Mar 18 15:11:02 1997 +0100
+++ b/src/Pure/library.ML Tue Mar 18 15:12:53 1997 +0100
@@ -919,22 +919,13 @@
in (x, zs) :: map step qs end;
-(** Simple random number generator; not guaranteed to be good, because modulus
- has been reduced from 2^31-1 to 2^29-1 to prevent integer overflows
-**)
-local val a = 16807.0 and m = 536870911.0 (* 2^29 - 1 *)
-in fun nextrandom seed =
- let val t = a*seed
- in t - m * real(floor(t/m)) end
-end;
-
(* generating identifiers *)
local
val a = ord "a" and z = ord "z" and A = ord "A" and Z = ord "Z"
and k0 = ord "0" and k9 = ord "9"
- val seedr = ref 10000.0;
+ val seedr = ref 0;
in
(*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
@@ -947,10 +938,10 @@
else (*i=63*) "'"
in implode (map char (radixpand (64,n))) end;
-(*Randomly generated identifiers with given prefix; MUST start with a letter*)
+(*Freshly generated identifiers with given prefix; MUST start with a letter*)
fun gensym pre = pre ^
- (#1(newid (floor (!seedr)),
- seedr := nextrandom (!seedr)))
+ (#1(newid (!seedr),
+ seedr := 1+ !seedr))
(*Increment a list of letters like a reversed base 26 number.
If head is "z", bumps chars in tail.