src/Pure/Thy/thy_header.ML
changeset 64556 851ae0e7b09c
parent 63936 b87784e19a77
child 65452 9e9750a7932c
--- 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 *)