tuned;
authorwenzelm
Thu, 12 May 2011 16:42:57 +0200
changeset 42719 a2e9872d5459
parent 42718 d7b2625c1193
child 42720 caa4f1279154
tuned;
src/Pure/General/yxml.scala
--- 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)
     }