# HG changeset patch
# User wenzelm
# Date 1310827872 -7200
# Node ID 33e20b7d7e7286db50c02aee85ad16313f314ea6
# Parent  16f2fd9103bda139690439a1d04039dd254a25aa
tuned;

diff -r 16f2fd9103bd -r 33e20b7d7e72 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Sat Jul 16 00:01:17 2011 +0200
+++ b/src/Pure/General/xml.ML	Sat Jul 16 16:51:12 2011 +0200
@@ -310,9 +310,10 @@
   | node t = raise XML_BODY [t];
 
 fun vector atts =
-  fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) 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);
 
-fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts))
+fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   | tagged t = raise XML_BODY [t];