removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);
authorwenzelm
Wed Apr 04 00:11:13 2007 +0200 (2007-04-04)
changeset 22582f315da9400fb
parent 22581 0a995d40160a
child 22583 4b1ecb19b411
removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Apr 04 00:11:12 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Apr 04 00:11:13 2007 +0200
     1.3 @@ -239,7 +239,6 @@
     1.4    val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
     1.5    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
     1.6    val gensym: string -> string
     1.7 -  val scanwords: (string -> bool) -> string list -> string list
     1.8    type stamp
     1.9    val stamp: unit -> stamp
    1.10    type serial
    1.11 @@ -777,10 +776,11 @@
    1.12    let
    1.13      val tab_width = 8;
    1.14  
    1.15 -    fun untab pos [] ys = rev ys 
    1.16 +    fun untab pos [] ys = rev ys
    1.17        | untab pos ("\n" :: xs) ys = untab 0 xs ("\n" :: ys)
    1.18        | untab pos ("\t" :: xs) ys =
    1.19 -          let val d = tab_width - (pos mod tab_width) in untab (pos + d) xs (replicate d " " @ ys) end
    1.20 +          let val d = tab_width - (pos mod tab_width)
    1.21 +          in untab (pos + d) xs (replicate d " " @ ys) end
    1.22        | untab pos (c :: xs) ys = untab (pos + 1) xs (c :: ys);
    1.23    in
    1.24      if not (exists (fn c => c = "\t") chs) then chs
    1.25 @@ -1131,7 +1131,7 @@
    1.26  (** Freshly generated identifiers; supplied prefix MUST start with a letter **)
    1.27  local
    1.28  (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
    1.29 -fun gensym_char i = 
    1.30 +fun gensym_char i =
    1.31    if i<26 then chr (ord "A" + i)
    1.32    else if i<52 then chr (ord "a" + i - 26)
    1.33    else chr (ord "0" + i - 52);
    1.34 @@ -1146,18 +1146,6 @@
    1.35  end;
    1.36  
    1.37  
    1.38 -(* lexical scanning *)
    1.39 -
    1.40 -(*scan a list of characters into "words" composed of "letters" (recognized by
    1.41 -  is_let) and separated by any number of non-"letters"*)
    1.42 -fun scanwords is_let cs =
    1.43 -  let fun scan1 [] = []
    1.44 -        | scan1 cs =
    1.45 -            let val (lets, rest) = take_prefix is_let cs
    1.46 -            in implode lets :: scanwords is_let rest end;
    1.47 -  in scan1 (#2 (take_prefix (not o is_let) cs)) end;
    1.48 -
    1.49 -
    1.50  (* stamps and serial numbers *)
    1.51  
    1.52  type stamp = unit ref;