src/Pure/General/symbol_pos.ML
changeset 32784 1a5dde5079ac
parent 30586 9674f64a0702
child 36957 cdb9e83abfbe
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Sep 30 19:04:48 2009 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Sep 30 22:20:58 2009 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4  
     1.5  fun pad [] = []
     1.6    | pad [(s, _)] = [s]
     1.7 -  | pad ((s1, pos1) :: (rest as (s2, pos2) :: _)) =
     1.8 +  | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
     1.9        let
    1.10          val end_pos1 = Position.advance s1 pos1;
    1.11          val d = Int.max (0, Position.distance_of end_pos1 pos2);