src/Pure/General/yxml.scala

--- a/src/Pure/General/yxml.scala	Sat Aug 13 13:42:35 2011 +0200
+++ b/src/Pure/General/yxml.scala	Sat Aug 13 13:48:26 2011 +0200
@@ -50,7 +50,7 @@
   private def err_element() = err("bad element")
   private def err_unbalanced(name: String) =
     if (name == "") err("unbalanced element")
-    else err("unbalanced element \"" + name + "\"")
+    else err("unbalanced element " + quote(name))
 
   private def parse_attrib(source: CharSequence) = {
     val s = source.toString