diff -r 9411ed32f3a7 -r a6dc270d3edb src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 12:23:51 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 13:42:35 2011 +0200
@@ -207,7 +207,10 @@
                 thy_header0 != thy_header
               case _ => true
             }
-          if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
+          if (update_header) {
+            doc_edits += (name -> Document.Node.Update_Header(header))
+            nodes += (name -> node.copy(header = header))
+          }
       }
       (doc_edits.toList, Document.Version(Document.new_id(), nodes))
     }