diff -r 6aa25b80e1a5 -r a21d3e1e64fd src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Thu Aug 11 18:01:28 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 11 20:32:44 2011 +0200
@@ -13,23 +13,24 @@
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.edit_version"
-    (fn [old_id_string, new_id_string, edits_yxml, headers_yxml] => Document.change_state (fn state =>
+    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let
         val old_id = Document.parse_id old_id_string;
         val new_id = Document.parse_id new_id_string;
-        val edits = YXML.parse_body edits_yxml |>
-          let open XML.Decode in
-            list (pair string
-              (variant
-               [fn ([], []) => Document.Remove,
-                fn ([], a) => Document.Edits (list (pair (option int) (option int)) a)]))
-          end;
-        val headers = YXML.parse_body headers_yxml |>
-          let open XML.Decode
-          in list (pair string (triple string (list string) (list string))) end;
+        val edits =
+          YXML.parse_body edits_yxml |>
+            let open XML.Decode in
+              list (pair string
+                (variant
+                 [fn ([], []) => Document.Remove,
+                  fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
+                  fn ([], a) =>
+                    Document.Update_Header (Exn.Res (triple string (list string) (list string) a)),
+                  fn ([a], []) => Document.Update_Header (Exn.Exn (ERROR a))]))
+            end;
 
       val await_cancellation = Document.cancel_execution state;
-      val (updates, state') = Document.edit old_id new_id edits headers state;
+      val (updates, state') = Document.edit old_id new_id edits state;
       val _ = await_cancellation ();
       val _ =
         Output.status (Markup.markup (Markup.assign new_id)