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