src/Pure/General/xml.scala

--- a/src/Pure/General/xml.scala	Tue May 11 23:09:49 2010 +0200
+++ b/src/Pure/General/xml.scala	Tue May 11 23:36:06 2010 +0200
@@ -92,12 +92,6 @@
     }
   }
 
-  def content_length(tree: XML.Tree): Int =
-    tree match {
-      case Elem(_, _, body) => (0 /: body)(_ + content_length(_))
-      case Text(s) => s.length
-    }
-
 
   /* cache for partial sharing -- NOT THREAD SAFE */