src/Pure/General/symbol_pos.ML
changeset 27984 b4dd58cff97c
parent 27864 827730aea9e8
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/General/symbol_pos.ML	Sun Aug 24 14:42:26 2008 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Sun Aug 24 17:23:42 2008 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  fun untabify ("\t", pos) =
     1.5        (case Position.column_of pos of
     1.6          SOME n => Symbol.spaces (tab_width - ((n - 1) mod tab_width))
     1.7 -      | NONE => error "No column information -- cannot interpret tabulators")
     1.8 +      | NONE => Symbol.space)
     1.9    | untabify (s, _) = s;
    1.10  
    1.11  val untabify_content = implode o map untabify;