src/Pure/General/symbol_pos.ML

--- a/src/Pure/General/symbol_pos.ML	Sat May 26 22:12:18 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun May 27 13:42:01 2018 +0200
@@ -40,6 +40,7 @@
   type text = string
   val implode: T list -> text
   val implode_range: Position.range -> T list -> text * Position.range
+  val explode_delete: text * Position.T -> T list * Position.T list
   val explode: text * Position.T -> T list
   val explode0: string -> T list
   val scan_ident: T list scanner
@@ -253,13 +254,17 @@
   let val syms' = (("", pos1) :: syms @ [("", pos2)])
   in (implode syms', range syms') end;
 
-fun explode (str, pos) =
+fun explode_delete (str, pos) =
   let
     val (res, _) =
       fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
         (Symbol.explode str) ([], Position.no_range_position pos);
-  in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
+  in
+    fold (fn (s, p) => if s = Symbol.DEL then apsnd (cons p) else apfst (cons (s, p)))
+      res ([], [])
+  end;
 
+val explode = explode_delete #> #1;
 fun explode0 str = explode (str, Position.none);