simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);

--- a/src/Pure/PIDE/xml.ML	Thu Mar 08 21:35:54 2012 +0100
+++ b/src/Pure/PIDE/xml.ML	Thu Mar 08 21:36:36 2012 +0100
@@ -360,8 +360,7 @@
   | node t = raise XML_BODY [t];
 
 fun vector atts =
-  #1 (fold_map (fn (a, x) =>
-        fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
+  map_index (fn (i, (a, x)) => if int_atom a = i then x else raise XML_ATOM a) atts;
 
 fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   | tagged t = raise XML_BODY [t];

--- a/src/Pure/PIDE/xml.scala	Thu Mar 08 21:35:54 2012 +0100
+++ b/src/Pure/PIDE/xml.scala	Thu Mar 08 21:36:36 2012 +0100
@@ -215,7 +215,7 @@
     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
 
     private def vector(xs: List[String]): XML.Attributes =
-      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
+      xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) })
 
     private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
       XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
@@ -293,15 +293,8 @@
       }
 
     private def vector(atts: XML.Attributes): List[String] =
-    {
-      val xs = new mutable.ListBuffer[String]
-      var i = 0
-      for ((a, x) <- atts) {
-        if (int_atom(a) == i) { xs += x; i = i + 1 }
-        else throw new XML_Atom(a)
-      }
-      xs.toList
-    }
+      atts.iterator.zipWithIndex.map(
+        { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList
 
     private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
       t match {