diff -r 9b5dadb0c28d -r 8a63c95b1d5b src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 00:21:19 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:00:22 2011 +0200
@@ -32,8 +32,8 @@
   }
 
   def make_xml_data(header: Header): XML.Body =
-    XML_Data.make_triple(XML_Data.make_string)(
-      XML_Data.make_list(XML_Data.make_string))(
+    XML_Data.make_triple(XML_Data.make_string,
+      XML_Data.make_list(XML_Data.make_string),
         XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)