# HG changeset patch
# User wenzelm
# Date 1261151556 -3600
# Node ID 17554065f3be1f9e53be0b310620a50c98c66ad0
# Parent  7492eca87ab4308aa67e7f7f073b9e6cb4de298b
tuned;

diff -r 7492eca87ab4 -r 17554065f3be src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Fri Dec 18 15:33:44 2009 +0100
+++ b/src/Pure/General/xml.scala	Fri Dec 18 16:52:36 2009 +0100
@@ -123,10 +123,12 @@
         case None => store(x)
       }
     def cache_props(x: List[(String, String)]): List[(String, String)] =
-      lookup(x) match {
-        case Some(y) => y
-        case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
-      }
+      if (x.isEmpty) x
+      else
+        lookup(x) match {
+          case Some(y) => y
+          case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
+        }
     def cache_tree(x: XML.Tree): XML.Tree =
       lookup(x) match {
         case Some(y) => y
@@ -138,10 +140,12 @@
           }
       }
     def cache_trees(x: List[XML.Tree]): List[XML.Tree] =
-      lookup(x) match {
-        case Some(y) => y
-        case None => x.map(cache_tree(_))
-      }
+      if (x.isEmpty) x
+      else
+        lookup(x) match {
+          case Some(y) => y
+          case None => x.map(cache_tree(_))
+        }
   }