# HG changeset patch
# User paulson
# Date 1172571035 -3600
# Node ID 0e0fe77d47684f63f3abb27c3066af137d49cecb
# Parent  6860f09242bf230e2ec68810c871e047ab177991
gensym no longer includes ' or _ in names (trailing _ is bad)

diff -r 6860f09242bf -r 0e0fe77d4768 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Feb 27 00:33:49 2007 +0100
+++ b/src/Pure/library.ML	Tue Feb 27 11:10:35 2007 +0100
@@ -1134,27 +1134,22 @@
 (* generating identifiers *)
 
 (** Freshly generated identifiers; supplied prefix MUST start with a letter **)
-local
 (*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
-fun char i =      if i<26 then chr (ord "A" + i)
-             else if i<52 then chr (ord "a" + i - 26)
-             else if i<62 then chr (ord"0" + i - 52)
-             else if i=62 then "_"
-             else  (*i=63*)    "'";
-
-val charVec = Vector.tabulate (64, char);
+fun gensym_char i = 
+  if i<26 then chr (ord "A" + i)
+  else if i<52 then chr (ord "a" + i - 26)
+  else if i<62 then chr (ord"0" + i - 52)
+  else if i=62 then "_"
+  else  (*i=63*)    "'";
 
-fun newid n =
-  let
-  in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end;
-
-val seedr = ref 0;
+val charVec = Vector.tabulate (64, gensym_char);
 
-in
+(*Not 64, as _ and ' could cause problems (especially _).*)
+fun newid n = implode (map (fn i => Vector.sub(charVec,i)) (radixpand (62,n)));
 
-fun gensym pre = pre ^ (#1(newid (!seedr), inc seedr));
+val gensym_seed = ref 0;
 
-end;
+fun gensym pre = pre ^ newid (inc gensym_seed);
 
 
 (* lexical scanning *)