src/Pure/library.ML
changeset 22368 0e0fe77d4768
parent 22256 23f3ca04d3b3
child 22369 a7263f330494
     1.1 --- a/src/Pure/library.ML	Tue Feb 27 00:33:49 2007 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Feb 27 11:10:35 2007 +0100
     1.3 @@ -1134,27 +1134,22 @@
     1.4  (* generating identifiers *)
     1.5  
     1.6  (** Freshly generated identifiers; supplied prefix MUST start with a letter **)
     1.7 -local
     1.8  (*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
     1.9 -fun char i =      if i<26 then chr (ord "A" + i)
    1.10 -             else if i<52 then chr (ord "a" + i - 26)
    1.11 -             else if i<62 then chr (ord"0" + i - 52)
    1.12 -             else if i=62 then "_"
    1.13 -             else  (*i=63*)    "'";
    1.14 -
    1.15 -val charVec = Vector.tabulate (64, char);
    1.16 +fun gensym_char i = 
    1.17 +  if i<26 then chr (ord "A" + i)
    1.18 +  else if i<52 then chr (ord "a" + i - 26)
    1.19 +  else if i<62 then chr (ord"0" + i - 52)
    1.20 +  else if i=62 then "_"
    1.21 +  else  (*i=63*)    "'";
    1.22  
    1.23 -fun newid n =
    1.24 -  let
    1.25 -  in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end;
    1.26 -
    1.27 -val seedr = ref 0;
    1.28 +val charVec = Vector.tabulate (64, gensym_char);
    1.29  
    1.30 -in
    1.31 +(*Not 64, as _ and ' could cause problems (especially _).*)
    1.32 +fun newid n = implode (map (fn i => Vector.sub(charVec,i)) (radixpand (62,n)));
    1.33  
    1.34 -fun gensym pre = pre ^ (#1(newid (!seedr), inc seedr));
    1.35 +val gensym_seed = ref 0;
    1.36  
    1.37 -end;
    1.38 +fun gensym pre = pre ^ newid (inc gensym_seed);
    1.39  
    1.40  
    1.41  (* lexical scanning *)