# HG changeset patch
# User wenzelm
# Date 1172618546 -3600
# Node ID a7263f3304943d199032e87473b0d0e1ba3bfbad
# Parent  0e0fe77d47684f63f3abb27c3066af137d49cecb
gensym: removed bits of dead code;

diff -r 0e0fe77d4768 -r a7263f330494 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Feb 27 11:10:35 2007 +0100
+++ b/src/Pure/library.ML	Wed Feb 28 00:22:26 2007 +0100
@@ -1134,22 +1134,21 @@
 (* generating identifiers *)
 
 (** Freshly generated identifiers; supplied prefix MUST start with a letter **)
-(*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
+local
+(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
 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*)    "'";
+  else chr (ord "0" + i - 52);
 
-val charVec = Vector.tabulate (64, gensym_char);
-
-(*Not 64, as _ and ' could cause problems (especially _).*)
-fun newid n = implode (map (fn i => Vector.sub(charVec,i)) (radixpand (62,n)));
+val char_vec = Vector.tabulate (62, gensym_char);
+fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
 
 val gensym_seed = ref 0;
 
-fun gensym pre = pre ^ newid (inc gensym_seed);
+in
+  fun gensym pre = pre ^ newid (inc gensym_seed);
+end;
 
 
 (* lexical scanning *)