changeset 32791 | 1a5dde5079ac |
parent 30589 | 9674f64a0702 |
child 36967 | 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);