diff -r fe6d1ae7a065 -r 9a35e88d9dc9 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Fri Aug 12 11:41:26 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 12 12:03:17 2011 +0200
@@ -150,7 +150,7 @@
             { case Document.Node.Remove() => (Nil, Nil) },
             { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
             { case Document.Node.Update_Header(
-                  Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) =>
+                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
                 (Nil, triple(string, list(string), list(string))(a, b, c)) },
             { case Document.Node.Update_Header(
                   Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))