1.1 --- a/src/Pure/library.ML	Wed Feb 20 00:53:53 2002 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Feb 20 00:54:54 2002 +0100
     1.3 @@ -281,9 +281,6 @@
     1.4    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
     1.5    val transitive_closure: (string * string list) list -> (string * string list) list
     1.6    val gensym: string -> string
     1.7 -  val bump_int_list: string list -> string list
     1.8 -  val bump_list: string list * string -> string list
     1.9 -  val bump_string: string -> string
    1.10    val scanwords: (string -> bool) -> string list -> string list
    1.11    datatype 'a mtree = Join of 'a * 'a mtree list
    1.12  end;
    1.13 @@ -1358,49 +1355,6 @@
    1.14  end;
    1.15  
    1.16  
    1.17 -local
    1.18 -(*Identifies those character codes legal in identifiers.
    1.19 -  chould use Basis Library character functions if Poly/ML provided characters*)
    1.20 -fun idCode k = (ord "a" <= k andalso k < ord "z") orelse
    1.21 -               (ord "A" <= k andalso k < ord "Z") orelse
    1.22 -               (ord "0" <= k andalso k < ord "9");
    1.23 -
    1.24 -val idCodeVec = Vector.tabulate (256, idCode);
    1.25 -
    1.26 -in
    1.27 -
    1.28 -(*Increment a list of letters like a reversed base 26 number.
    1.29 -  If head is "z", bumps chars in tail.
    1.30 -  Digits are incremented as if they were integers.
    1.31 -  "_" and "'" are not changed.
    1.32 -  For making variants of identifiers.*)
    1.33 -
    1.34 -fun bump_int_list(c::cs) =
    1.35 -        if c="9" then "0" :: bump_int_list cs
    1.36 -        else
    1.37 -        if "0" <= c andalso c < "9" then chr(ord(c)+1) :: cs
    1.38 -        else "1" :: c :: cs
    1.39 -  | bump_int_list([]) = error("bump_int_list: not an identifier");
    1.40 -
    1.41 -fun bump_list([], d) = [d]
    1.42 -  | bump_list(["'"], d) = [d, "'"]
    1.43 -  | bump_list("z"::cs, _) = "a" :: bump_list(cs, "a")
    1.44 -  | bump_list("Z"::cs, _) = "A" :: bump_list(cs, "A")
    1.45 -  | bump_list("9"::cs, _) = "0" :: bump_int_list cs
    1.46 -  | bump_list(c::cs, _) =
    1.47 -        let val k = ord(c)
    1.48 -        in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs
    1.49 -           else
    1.50 -           if c="'" orelse c="_" then c :: bump_list(cs, "")
    1.51 -           else error("bump_list: not legal in identifier: " ^
    1.52 -                      implode(rev(c::cs)))
    1.53 -        end;
    1.54 -
    1.55 -end;
    1.56 -
    1.57 -fun bump_string s : string = implode (rev (bump_list(rev(explode s), "")));
    1.58 -
    1.59 -
    1.60  (* lexical scanning *)
    1.61  
    1.62  (*scan a list of characters into "words" composed of "letters" (recognized by