src/Pure/Thy/thy_header.scala

 object Thy_Header extends Parse.Parser
 {
   /* bootstrap keywords */
 
   type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
-
-  val HEADER = "header"  /* FIXME legacy */
 
   val CHAPTER = "chapter"
   val SECTION = "section"
   val SUBSECTION = "subsection"
   val SUBSUBSECTION = "subsubsection"

       ("==", None, None),
       (AND, None, None),
       (BEGIN, None, None),
       (IMPORTS, None, None),
       (KEYWORDS, None, None),
-      (HEADER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
       (CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
       (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
       (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
       (SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
       (PARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),

         { case None => Nil case Some(_ ~ xs) => xs }) ~
       $$$(BEGIN) ^^
       { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
 
     val heading =
-      (command(HEADER) |
-        command(CHAPTER) |
+      (command(CHAPTER) |
         command(SECTION) |
         command(SUBSECTION) |
         command(SUBSUBSECTION) |
         command(PARAGRAPH) |
         command(SUBPARAGRAPH) |