src/Pure/PIDE/xml.ML

--- 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];