# HG changeset patch
# User wenzelm
# Date 1310494260 -7200
# Node ID ef45eaf2775f6f38d5611bbdd3b23330426a1268
# Parent  834de29572d517078b68a899802c5b8f13079df2
made SML/NJ happy;

diff -r 834de29572d5 -r ef45eaf2775f src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Tue Jul 12 19:49:35 2011 +0200
+++ b/src/Pure/General/xml.ML	Tue Jul 12 20:11:00 2011 +0200
@@ -304,8 +304,8 @@
 fun node (Elem ((":", []), ts)) = ts
   | node t = raise XML_BODY [t];
 
-val vector =
-  fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a);
+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;
 
 fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts))
   | tagged t = raise XML_BODY [t];