src/Pure/General/xml.ML

--- a/src/Pure/General/xml.ML	Tue Jul 12 10:44:30 2011 +0200
+++ b/src/Pure/General/xml.ML	Tue Jul 12 11:16:56 2011 +0200
@@ -324,7 +324,11 @@
   | option f [t] = SOME (f (node t))
   | option _ ts = raise XML_BODY ts;
 
-fun variant fs [t] = uncurry (nth fs) (tagged t)
+fun variant fs [t] =
+      let
+        val (tag, ts) = tagged t;
+        val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
+      in f ts end
   | variant _ ts = raise XML_BODY ts;
 
 end;