diff -r 7c4793e39dd5 -r 6e40f5d43936 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sun May 13 21:59:41 2018 +0200
+++ b/src/Pure/General/symbol_pos.ML	Mon May 14 09:39:27 2018 +0200
@@ -244,7 +244,7 @@
   | 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);
+        val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2)));
       in s1 :: replicate d Symbol.DEL @ pad rest end;
 
 val implode = implode o pad;