src/Pure/Tools/build.scala

--- a/src/Pure/Tools/build.scala	Tue Apr 09 20:16:52 2013 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 09 20:27:27 2013 +0200
@@ -595,7 +595,7 @@
     val lines = split_lines(text)
     val xml_cache = new XML.Cache()
     def parse_lines(prfx: String): List[Properties.T] =
-      Props.parse_lines(prfx, lines).map(xml_cache.cache_props)
+      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
 
     val name =
       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""