# HG changeset patch
# User wenzelm
# Date 1218653840 -7200
# Node ID 49503146b853f68b79c560f6259c81f97f51df91
# Parent  c749054238951d9f8d396c2a7559f9d9b9a87074
removed obsolete untabify (superceded by SymbolPos.tabify_content);

diff -r c74905423895 -r 49503146b853 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Aug 13 20:57:18 2008 +0200
+++ b/src/Pure/library.ML	Wed Aug 13 20:57:20 2008 +0200
@@ -152,7 +152,6 @@
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
   val prefix_lines: string -> string -> string
-  val untabify: string list -> string list
   val prefix: string -> string -> string
   val suffix: string -> string -> string
   val unprefix: string -> string -> string
@@ -757,21 +756,6 @@
 fun prefix_lines "" txt = txt
   | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
 
-fun untabify chs =
-  let
-    val tab_width = 8;
-
-    fun untab pos [] ys = rev ys
-      | untab pos ("\n" :: xs) ys = untab 0 xs ("\n" :: ys)
-      | untab pos ("\t" :: xs) ys =
-          let val d = tab_width - (pos mod tab_width)
-          in untab (pos + d) xs (funpow d (cons " ") ys) end
-      | untab pos (c :: xs) ys = untab (pos + 1) xs (c :: ys);
-  in
-    if not (exists (fn c => c = "\t") chs) then chs
-    else untab 0 chs []
-  end;
-
 fun prefix prfx s = prfx ^ s;
 fun suffix sffx s = s ^ sffx;