# HG changeset patch
# User paulson
# Date 843493376 -7200
# Node ID b48f066d52dc88d12a314160309d142ed737a081
# Parent  ed423882c6a9ec2cd54aea16c5727bae614a9afc
Addition of gensym

diff -r ed423882c6a9 -r b48f066d52dc src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Sep 23 17:41:57 1996 +0200
+++ b/src/Pure/library.ML	Mon Sep 23 17:42:56 1996 +0200
@@ -905,13 +905,40 @@
       in (x, zs) :: map step qs end;
 
 
+(** Recommended by Stephen K. Park and Keith W. Miller, 
+      Random number generators: good ones are hard to find,
+      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
+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;
 in
 
+(*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
+fun newid n = 
+  let fun char i =
+               if i<26 then chr (A+i)
+          else if i<52 then chr (a+i-26)
+          else if i<62 then chr (k0+i-52)
+          else if i=62 then "_"
+          else  (*i=63*)    "'"
+  in  implode (map char (radixpand (64,n)))  end;
+
+(*Randomly generated identifiers with given prefix; MUST start with a letter*)
+fun gensym pre = pre ^ 
+                 (#1(newid (floor (!seedr)), seedr := nextrandom (!seedr)))
+
 (*Increment a list of letters like a reversed base 26 number.
   If head is "z", bumps chars in tail.
   Digits are incremented as if they were integers.