src/Pure/Thy/thy_header.ML
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),