src/Pure/General/yxml.scala

 
     /* stack operations */
 
     var stack: List[((String, XML.Attributes), List[XML.Tree])] = null
 
-    def add(x: XML.Tree) = stack match {
+    def add(x: XML.Tree) = (stack: @unchecked) match {
       case ((elem, body) :: pending) => stack = (elem, x :: body) :: pending
     }
 
     def push(name: String, atts: XML.Attributes) =
       if (name == "") err_element()
       else stack = ((name, atts), Nil) :: stack
 
-    def pop() = stack match {
+    def pop() = (stack: @unchecked) match {
       case ((("", _), _) :: _) => err_unbalanced("")
       case (((name, atts), body) :: pending) =>
         stack = pending; add(XML.Elem(name, atts, body.reverse))
     }