src/Pure/General/symbol_pos.ML
changeset 41416 a2208d3e2bd6
parent 40525 14a2e686bdac
child 42503 27514b6fbe93
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Dec 29 20:41:33 2010 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Dec 29 21:21:11 2010 +0100
     1.3 @@ -174,9 +174,11 @@
     1.4    in (implode syms', range syms') end;
     1.5  
     1.6  fun explode (str, pos) =
     1.7 -  fold_map (fn s => fn p => ((s, p), (Position.advance s p)))
     1.8 -    (Symbol.explode str) (Position.reset_range pos)
     1.9 -  |> #1 |> filter_out (fn (s, _) => s = Symbol.DEL);
    1.10 +  let
    1.11 +    val (res, _) =
    1.12 +      fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
    1.13 +        (Symbol.explode str) ([], Position.reset_range pos);
    1.14 +  in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
    1.15  
    1.16  end;
    1.17