# HG changeset patch
# User wenzelm
# Date 1293654071 -3600
# Node ID a2208d3e2bd65fed8a0b9c1cd75eec7244d86faf
# Parent  23533273220a59d82002910a2703c7897a1513a5
more scalable Symbol_Pos.explode;

diff -r 23533273220a -r a2208d3e2bd6 src/Pure/General/symbol_pos.ML
--- 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;