XML.Cache: intern property keys once and for all (again);

--- a/src/Pure/General/xml.scala	Sat Aug 28 20:24:41 2010 +0200
+++ b/src/Pure/General/xml.scala	Sat Aug 28 22:58:24 2010 +0200
@@ -112,7 +112,7 @@
         else
           lookup(x) match {
             case Some(y) => y
-            case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
+            case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2))))
           }
       def cache_markup(x: Markup): Markup =
         lookup(x) match {