# HG changeset patch
# User wenzelm
# Date 1305211377 -7200
# Node ID a2e9872d5459e5a91291fa872ac0e9205b471a2a
# Parent  d7b2625c11934b84cf023fe13be603741d6998ed
tuned;

diff -r d7b2625c1193 -r a2e9872d5459 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)
     }