src/Pure/Thy/thy_header.ML
changeset 63448 998acd66fbd7
parent 63429 baedd4724f08
child 63449 b3f6e81cd13b
--- a/src/Pure/Thy/thy_header.ML	Mon Jul 11 18:30:07 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML	Mon Jul 11 18:39:30 2016 +0200
@@ -71,8 +71,8 @@
      (("==", @{here}), Keyword.no_spec),
      (("and", @{here}), Keyword.no_spec),
      ((beginN, @{here}), Keyword.no_spec),
-     ((importsN, @{here}), Keyword.no_spec),
-     ((keywordsN, @{here}), Keyword.no_spec),
+     ((importsN, @{here}), Keyword.quasi_command_spec),
+     ((keywordsN, @{here}), Keyword.quasi_command_spec),
      ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
      ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
      ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),