--- a/src/Pure/Thy/thy_header.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Thy/thy_header.ML Tue Dec 13 11:51:42 2016 +0100
@@ -64,28 +64,28 @@
val bootstrap_keywords =
Keyword.empty_keywords
|> Keyword.add_keywords
- [(("%", @{here}), Keyword.no_spec),
- (("(", @{here}), Keyword.no_spec),
- ((")", @{here}), Keyword.no_spec),
- ((",", @{here}), Keyword.no_spec),
- (("::", @{here}), Keyword.no_spec),
- (("=", @{here}), Keyword.no_spec),
- (("and", @{here}), Keyword.no_spec),
- ((beginN, @{here}), Keyword.quasi_command_spec),
- ((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, []), [])),
- ((theoryN, @{here}), ((Keyword.thy_begin, []), ["theory"])),
- (("ML", @{here}), ((Keyword.thy_decl, []), ["ML"]))];
+ [(("%", \<^here>), Keyword.no_spec),
+ (("(", \<^here>), Keyword.no_spec),
+ ((")", \<^here>), Keyword.no_spec),
+ ((",", \<^here>), Keyword.no_spec),
+ (("::", \<^here>), Keyword.no_spec),
+ (("=", \<^here>), Keyword.no_spec),
+ (("and", \<^here>), Keyword.no_spec),
+ ((beginN, \<^here>), Keyword.quasi_command_spec),
+ ((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, []), [])),
+ ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
+ (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];
(* theory data *)