# HG changeset patch
# User wenzelm
# Date 1289385875 -3600
# Node ID a81346e57ceff95b83faa556a803cf0bbb79100e
# Parent  45e7c2889d2f90f9d6437b07a80cc21360212548
tuned;

diff -r 45e7c2889d2f -r a81346e57cef src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Tue Nov 09 23:24:46 2010 +0100
+++ b/src/Pure/General/yxml.scala	Wed Nov 10 11:44:35 2010 +0100
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import scala.collection.mutable.ListBuffer
+import scala.collection.mutable
 
 
 object YXML
@@ -84,8 +84,8 @@
   {
     /* stack operations */
 
-    def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
-    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
+    def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
+    var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
 
     def add(x: XML.Tree)
     {