src/Pure/General/symbol_pos.ML
changeset 27864 827730aea9e8
parent 27852 6454fef6a293
child 27984 b4dd58cff97c
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Aug 13 20:57:40 2008 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Aug 14 11:55:05 2008 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  val content = implode o map symbol;
     1.5  
     1.6  
     1.7 -val tab_width = 8;
     1.8 +val tab_width = (8: int);
     1.9  
    1.10  fun untabify ("\t", pos) =
    1.11        (case Position.column_of pos of