tuned signature;

--- a/src/Pure/General/xml.scala	Fri Dec 18 11:28:24 2009 +0100
+++ b/src/Pure/General/xml.scala	Fri Dec 18 11:44:25 2009 +0100
@@ -127,20 +127,20 @@
         case Some(y) => y
         case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
       }
-    def apply(x: XML.Tree): XML.Tree =
+    def cache_tree(x: XML.Tree): XML.Tree =
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
             case XML.Elem(name, props, body) =>
-              store(XML.Elem(cache_string(name), cache_props(props), apply(body)))
+              store(XML.Elem(cache_string(name), cache_props(props), cache_trees(body)))
             case XML.Text(text) => XML.Text(cache_string(text))
           }
       }
-    def apply(x: List[XML.Tree]): List[XML.Tree] =
+    def cache_trees(x: List[XML.Tree]): List[XML.Tree] =
       lookup(x) match {
         case Some(y) => y
-        case None => x.map(apply(_))
+        case None => x.map(cache_tree(_))
       }
   }
 

--- a/src/Pure/System/isabelle_process.scala	Fri Dec 18 11:28:24 2009 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Dec 18 11:44:25 2009 +0100
@@ -101,8 +101,8 @@
     def is_control = Kind.is_control(kind)
     def is_system = Kind.is_system(kind)
 
-    def cache(table: XML.Cache): Result =
-      new Result(kind, table.cache_props(props), table(body))
+    def cache(c: XML.Cache): Result =
+      new Result(kind, c.cache_props(props), c.cache_trees(body))
   }
 }