1.1 --- a/src/Pure/library.ML	Wed Aug 13 20:57:18 2008 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Aug 13 20:57:20 2008 +0200
     1.3 @@ -152,7 +152,6 @@
     1.4    val space_explode: string -> string -> string list
     1.5    val split_lines: string -> string list
     1.6    val prefix_lines: string -> string -> string
     1.7 -  val untabify: string list -> string list
     1.8    val prefix: string -> string -> string
     1.9    val suffix: string -> string -> string
    1.10    val unprefix: string -> string -> string
    1.11 @@ -757,21 +756,6 @@
    1.12  fun prefix_lines "" txt = txt
    1.13    | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
    1.14  
    1.15 -fun untabify chs =
    1.16 -  let
    1.17 -    val tab_width = 8;
    1.18 -
    1.19 -    fun untab pos [] ys = rev ys
    1.20 -      | untab pos ("\n" :: xs) ys = untab 0 xs ("\n" :: ys)
    1.21 -      | untab pos ("\t" :: xs) ys =
    1.22 -          let val d = tab_width - (pos mod tab_width)
    1.23 -          in untab (pos + d) xs (funpow d (cons " ") ys) end
    1.24 -      | untab pos (c :: xs) ys = untab (pos + 1) xs (c :: ys);
    1.25 -  in
    1.26 -    if not (exists (fn c => c = "\t") chs) then chs
    1.27 -    else untab 0 chs []
    1.28 -  end;
    1.29 -
    1.30  fun prefix prfx s = prfx ^ s;
    1.31  fun suffix sffx s = s ^ sffx;
    1.32