--- a/src/Pure/Thy/thy_header.ML Sun Feb 28 15:57:03 2016 +0100
+++ b/src/Pure/Thy/thy_header.ML Sun Feb 28 17:37:20 2016 +0100
@@ -42,8 +42,6 @@
(* bootstrap keywords *)
-val headerN = "header"; (* FIXME legacy *)
-
val chapterN = "chapter";
val sectionN = "section";
val subsectionN = "subsection";
@@ -72,7 +70,6 @@
((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, []), [])),
@@ -147,8 +144,7 @@
(* read header *)
val heading =
- (Parse.command headerN ||
- Parse.command chapterN ||
+ (Parse.command chapterN ||
Parse.command sectionN ||
Parse.command subsectionN ||
Parse.command subsubsectionN ||