src/Pure/General/yxml.scala
changeset 42719 a2e9872d5459
parent 40453 a81346e57cef
child 43650 f00da558b78e
--- a/src/Pure/General/yxml.scala	Thu May 12 16:28:46 2011 +0200
+++ b/src/Pure/General/yxml.scala	Thu May 12 16:42:57 2011 +0200
@@ -121,7 +121,7 @@
         }
       }
     }
-    stack match {
+    (stack: @unchecked) match {
       case List((Markup.Empty, body)) => body.toList
       case (Markup(name, _), _) :: _ => err_unbalanced(name)
     }