diff -r e43d761a742d -r 1a5dde5079ac src/Pure/General/symbol_pos.ML
--- 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);