diff -r 9b5dadb0c28d -r 8a63c95b1d5b src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Sun Jul 10 00:21:19 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 13:00:22 2011 +0200
@@ -144,14 +144,14 @@
   {
     val arg1 =
       XML_Data.make_list(
-        XML_Data.make_pair(XML_Data.make_string)(
+        XML_Data.make_pair(XML_Data.make_string,
           XML_Data.make_option(XML_Data.make_list(
               XML_Data.make_pair(
-                XML_Data.make_option(XML_Data.make_long))(
+                XML_Data.make_option(XML_Data.make_long),
                 XML_Data.make_option(XML_Data.make_long))))))(edits)
 
     val arg2 =
-      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string)(Thy_Header.make_xml_data))(headers)
+      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string, Thy_Header.make_xml_data))(headers)
 
     input("Isar_Document.edit_version",
       Document.ID(old_id), Document.ID(new_id),