changeset 58920 | 2f8168dc0eac |
parent 58918 | 8d36bc5eaed3 |
child 58924 | b48bbd380d59 |
--- a/src/Pure/Thy/thy_header.ML Thu Nov 06 13:36:19 2014 +0100 +++ b/src/Pure/Thy/thy_header.ML Thu Nov 06 13:44:14 2014 +0100 @@ -79,9 +79,9 @@ val header_keywords = Keyword.empty_keywords - |> fold (Keyword.add o rpair NONE) + |> fold (Keyword.add_keywords o rpair NONE) ["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN] - |> fold Keyword.add + |> fold Keyword.add_keywords [(headerN, SOME Keyword.heading), (chapterN, SOME Keyword.heading), (sectionN, SOME Keyword.heading),