src/Pure/Thy/thy_header.ML
changeset 58907 0ee3563803c9
parent 58904 f49c4f883c58
child 58908 58bedbc18915
--- a/src/Pure/Thy/thy_header.ML	Wed Nov 05 21:21:15 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Wed Nov 05 21:59:21 2014 +0100
@@ -81,9 +81,13 @@
   Keyword.empty_keywords
   |> fold (Keyword.add o rpair NONE)
     ["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN]
-  |> fold (Keyword.add o rpair (SOME Keyword.heading))
-    [headerN, chapterN, sectionN, subsectionN, subsubsectionN]
-  |> Keyword.add (theoryN, SOME Keyword.thy_begin);
+  |> fold Keyword.add
+    [(headerN, SOME Keyword.heading),
+     (chapterN, SOME Keyword.heading),
+     (sectionN, SOME Keyword.heading),
+     (subsectionN, SOME Keyword.heading),
+     (subsubsectionN, SOME Keyword.heading),
+     (theoryN, SOME Keyword.thy_begin)];
 
 
 (* header args *)