src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/Thy/thy_header.scala	Tue Jul 12 10:44:30 2011 +0200
@@ -31,10 +31,10 @@
       Header(f(name), imports.map(f), uses.map(f))
   }
 
-  val encode_xml_data: XML_Data.Encode.T[Header] =
+  val xml_encode: XML.Encode.T[Header] =
   {
     case Header(name, imports, uses) =>
-      import XML_Data.Encode._
+      import XML.Encode._
       triple(string, list(string), list(string))(name, imports, uses)
   }