--- a/src/Pure/Thy/thy_header.ML Tue Dec 05 15:29:37 2017 +0100
+++ b/src/Pure/Thy/thy_header.ML Tue Dec 05 15:55:14 2017 +0100
@@ -77,15 +77,15 @@
((importsN, \<^here>), Keyword.quasi_command_spec),
((keywordsN, \<^here>), Keyword.quasi_command_spec),
((abbrevsN, \<^here>), Keyword.quasi_command_spec),
- ((chapterN, \<^here>), ((Keyword.document_heading, []), [])),
- ((sectionN, \<^here>), ((Keyword.document_heading, []), [])),
- ((subsectionN, \<^here>), ((Keyword.document_heading, []), [])),
- ((subsubsectionN, \<^here>), ((Keyword.document_heading, []), [])),
- ((paragraphN, \<^here>), ((Keyword.document_heading, []), [])),
- ((subparagraphN, \<^here>), ((Keyword.document_heading, []), [])),
- ((textN, \<^here>), ((Keyword.document_body, []), [])),
- ((txtN, \<^here>), ((Keyword.document_body, []), [])),
- ((text_rawN, \<^here>), ((Keyword.document_raw, []), [])),
+ ((chapterN, \<^here>), Keyword.document_heading_spec),
+ ((sectionN, \<^here>), Keyword.document_heading_spec),
+ ((subsectionN, \<^here>), Keyword.document_heading_spec),
+ ((subsubsectionN, \<^here>), Keyword.document_heading_spec),
+ ((paragraphN, \<^here>), Keyword.document_heading_spec),
+ ((subparagraphN, \<^here>), Keyword.document_heading_spec),
+ ((textN, \<^here>), Keyword.document_body_spec),
+ ((txtN, \<^here>), Keyword.document_body_spec),
+ ((text_rawN, \<^here>), ((Keyword.document_raw, []), ["document"])),
((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
(("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];