src/Pure/General/xml.scala
changeset 43768 d52ab827d62b
parent 43767 e0219ef7f84c
child 43778 ce9189450447
--- 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)
     }
   }