src/Pure/Thy/thy_header.ML
changeset 67136 1368cfa92b7a
parent 67013 335a7dce7cb3
child 67139 8fe0aba577af
     1.1 --- a/src/Pure/Thy/thy_header.ML	Mon Dec 04 23:10:52 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Dec 05 14:03:10 2017 +0100
     1.3 @@ -160,19 +160,19 @@
     1.4  (* read header *)
     1.5  
     1.6  val heading =
     1.7 -  (Parse.command chapterN ||
     1.8 -    Parse.command sectionN ||
     1.9 -    Parse.command subsectionN ||
    1.10 -    Parse.command subsubsectionN ||
    1.11 -    Parse.command paragraphN ||
    1.12 -    Parse.command subparagraphN ||
    1.13 -    Parse.command textN ||
    1.14 -    Parse.command txtN ||
    1.15 -    Parse.command text_rawN) --
    1.16 +  (Parse.command_name chapterN ||
    1.17 +    Parse.command_name sectionN ||
    1.18 +    Parse.command_name subsectionN ||
    1.19 +    Parse.command_name subsubsectionN ||
    1.20 +    Parse.command_name paragraphN ||
    1.21 +    Parse.command_name subparagraphN ||
    1.22 +    Parse.command_name textN ||
    1.23 +    Parse.command_name txtN ||
    1.24 +    Parse.command_name text_rawN) --
    1.25    Parse.tags -- Parse.!!! Parse.document_source;
    1.26  
    1.27  val header =
    1.28 -  (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
    1.29 +  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
    1.30  
    1.31  fun token_source pos =
    1.32    Symbol.explode