more precise exceptions;

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

--- a/src/Pure/General/xml.scala	Tue Jul 12 10:44:30 2011 +0200
+++ b/src/Pure/General/xml.scala	Tue Jul 12 11:16:56 2011 +0200
@@ -361,7 +361,10 @@
     {
       case List(t) =>
         val (tag, ts) = tagged(t)
-        fs(tag)(ts)
+        val f =
+          try { fs(tag) }
+          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
+        f(ts)
       case ts => throw new XML_Body(ts)
     }
   }