diff -r ae2906662eec -r 6aa25b80e1a5 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Thu Aug 11 13:24:49 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 11 18:01:28 2011 +0200
@@ -18,8 +18,12 @@
         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 (option (list (pair (option int) (option int))))) end;
+          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;