src/Pure/Thy/thy_header.ML

   {name = name, imports = imports, keywords = keywords};
 
 
 (* bootstrap keywords *)
 
-val headerN = "header";  (* FIXME legacy *)
-
 val chapterN = "chapter";
 val sectionN = "section";
 val subsectionN = "subsection";
 val subsubsectionN = "subsubsection";
 val paragraphN = "paragraph";

      (("==", @{here}), NONE),
      (("and", @{here}), NONE),
      ((beginN, @{here}), NONE),
      ((importsN, @{here}), NONE),
      ((keywordsN, @{here}), NONE),
-     ((headerN, @{here}), SOME ((Keyword.document_heading, []), [])),
      ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
      ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
      ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
      ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
      ((paragraphN, @{here}), SOME ((Keyword.document_heading, []), [])),

 
 
 (* read header *)
 
 val heading =
-  (Parse.command headerN ||
-    Parse.command chapterN ||
+  (Parse.command chapterN ||
     Parse.command sectionN ||
     Parse.command subsectionN ||
     Parse.command subsubsectionN ||
     Parse.command paragraphN ||
     Parse.command subparagraphN ||