src/Pure/General/yxml.scala

--- a/src/Pure/General/yxml.scala	Mon Jan 19 13:38:59 2009 +0100
+++ b/src/Pure/General/yxml.scala	Mon Jan 19 16:03:04 2009 +0100
@@ -59,7 +59,7 @@
     val s = source.toString
     val i = s.indexOf('=')
     if (i <= 0) err_attribute()
-    (s.substring(0, i), s.substring(i + 1))
+    (s.substring(0, i).intern, s.substring(i + 1))
   }
 
 
@@ -91,7 +91,7 @@
       if (chunk == Y_string) pop()
       else {
         chunks(Y, chunk).toList match {
-          case "" :: name :: atts => push(name.toString, atts.map(parse_attrib))
+          case "" :: name :: atts => push(name.toString.intern, atts.map(parse_attrib))
           case txts => for (txt <- txts) add(XML.Text(txt.toString))
         }
       }