src/Pure/Thy/thy_header.ML
changeset 58908 58bedbc18915
parent 58907 0ee3563803c9
child 58918 8d36bc5eaed3
--- a/src/Pure/Thy/thy_header.ML	Wed Nov 05 21:59:21 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Wed Nov 05 22:17:05 2014 +0100
@@ -131,15 +131,15 @@
 (* read header *)
 
 val heading =
-  (Parse.command_name headerN ||
-    Parse.command_name chapterN ||
-    Parse.command_name sectionN ||
-    Parse.command_name subsectionN ||
-    Parse.command_name subsubsectionN) --
+  (Parse.command headerN ||
+    Parse.command chapterN ||
+    Parse.command sectionN ||
+    Parse.command subsectionN ||
+    Parse.command subsubsectionN) --
   Parse.tags -- Parse.!!! Parse.document_source;
 
 val header =
-  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
+  (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
 
 fun token_source pos str =
   str