# HG changeset patch
# User paulson
# Date 858694373 -3600
# Node ID 772f6bba48a1379cb1339ddebd8f615ab91fc670
# Parent  6e5b2d6503ebde57e6e21eaef1db5e9f95de0e78
gensym no longer generates random identifiers, but just enumerates them
starting from A.  The random number generator was needlessly slow and caused
portability problems.

diff -r 6e5b2d6503eb -r 772f6bba48a1 src/Pure/library.ML
--- 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.