1.1 --- a/src/Pure/library.ML	Tue Feb 06 19:32:32 2007 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Feb 07 12:05:54 2007 +0100
     1.3 @@ -782,13 +782,14 @@
     1.4    let
     1.5      val tab_width = 8;
     1.6  
     1.7 -    fun untab (_, "\n") = (0, ["\n"])
     1.8 -      | untab (pos, "\t") =
     1.9 -          let val d = tab_width - (pos mod tab_width) in (pos + d, replicate d " ") end
    1.10 -      | untab (pos, c) = (pos + 1, [c]);
    1.11 +    fun untab pos [] ys = rev ys 
    1.12 +      | untab pos ("\n" :: xs) ys = untab 0 xs ("\n" :: ys)
    1.13 +      | untab pos ("\t" :: xs) ys =
    1.14 +          let val d = tab_width - (pos mod tab_width) in untab (pos + d) xs (replicate d " " @ ys) end
    1.15 +      | untab pos (c :: xs) ys = untab (pos + 1) xs (c :: ys);
    1.16    in
    1.17      if not (exists (fn c => c = "\t") chs) then chs
    1.18 -    else flat (#2 (foldl_map untab (0, chs)))
    1.19 +    else untab 0 chs []
    1.20    end;
    1.21  
    1.22  fun prefix prfx s = prfx ^ s;