# HG changeset patch
# User wenzelm
# Date 1014162894 -3600
# Node ID 58da1dc2720cde8d0b5e5e1cc3bef8fb86f1daf7
# Parent  a23dc0b7566f40eb54e7b7db98b3ea2f2541b1bc
removed obscure functions bump_int_list, bump_list, bump_string;

diff -r a23dc0b7566f -r 58da1dc2720c src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Feb 20 00:53:53 2002 +0100
+++ b/src/Pure/library.ML	Wed Feb 20 00:54:54 2002 +0100
@@ -281,9 +281,6 @@
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   val transitive_closure: (string * string list) list -> (string * string list) list
   val gensym: string -> string
-  val bump_int_list: string list -> string list
-  val bump_list: string list * string -> string list
-  val bump_string: string -> string
   val scanwords: (string -> bool) -> string list -> string list
   datatype 'a mtree = Join of 'a * 'a mtree list
 end;
@@ -1358,49 +1355,6 @@
 end;
 
 
-local
-(*Identifies those character codes legal in identifiers.
-  chould use Basis Library character functions if Poly/ML provided characters*)
-fun idCode k = (ord "a" <= k andalso k < ord "z") orelse
-               (ord "A" <= k andalso k < ord "Z") orelse
-               (ord "0" <= k andalso k < ord "9");
-
-val idCodeVec = Vector.tabulate (256, idCode);
-
-in
-
-(*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.
-  "_" and "'" are not changed.
-  For making variants of identifiers.*)
-
-fun bump_int_list(c::cs) =
-        if c="9" then "0" :: bump_int_list cs
-        else
-        if "0" <= c andalso c < "9" then chr(ord(c)+1) :: cs
-        else "1" :: c :: cs
-  | bump_int_list([]) = error("bump_int_list: not an identifier");
-
-fun bump_list([], d) = [d]
-  | bump_list(["'"], d) = [d, "'"]
-  | bump_list("z"::cs, _) = "a" :: bump_list(cs, "a")
-  | bump_list("Z"::cs, _) = "A" :: bump_list(cs, "A")
-  | bump_list("9"::cs, _) = "0" :: bump_int_list cs
-  | bump_list(c::cs, _) =
-        let val k = ord(c)
-        in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs
-           else
-           if c="'" orelse c="_" then c :: bump_list(cs, "")
-           else error("bump_list: not legal in identifier: " ^
-                      implode(rev(c::cs)))
-        end;
-
-end;
-
-fun bump_string s : string = implode (rev (bump_list(rev(explode s), "")));
-
-
 (* lexical scanning *)
 
 (*scan a list of characters into "words" composed of "letters" (recognized by