more scalable Symbol_Pos.explode;

--- a/src/Pure/General/symbol_pos.ML	Wed Dec 29 20:41:33 2010 +0100
+++ b/src/Pure/General/symbol_pos.ML	Wed Dec 29 21:21:11 2010 +0100
@@ -174,9 +174,11 @@
   in (implode syms', range syms') end;
 
 fun explode (str, pos) =
-  fold_map (fn s => fn p => ((s, p), (Position.advance s p)))
-    (Symbol.explode str) (Position.reset_range pos)
-  |> #1 |> filter_out (fn (s, _) => s = Symbol.DEL);
+  let
+    val (res, _) =
+      fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
+        (Symbol.explode str) ([], Position.reset_range pos);
+  in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
 
 end;