--- a/src/Pure/General/xml.scala Thu Dec 18 09:30:36 2008 -0800 +++ b/src/Pure/General/xml.scala Fri Dec 19 20:37:29 2008 +0100 @@ -1,5 +1,4 @@ /* Title: Pure/General/xml.scala - ID: $Id$ Author: Makarius Simple XML tree values.