--- a/src/Pure/Thy/thy_header.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/thy_header.ML Sun Mar 10 21:12:29 2019 +0100
@@ -175,10 +175,10 @@
Parse.command_name textN ||
Parse.command_name txtN ||
Parse.command_name text_rawN) --
- Document_Source.annotation -- Parse.!!! Parse.document_source;
+ (Document_Source.annotation |-- Parse.!!! Parse.document_source);
val parse_header =
- (Scan.repeat heading -- Parse.command_name theoryN -- Document_Source.annotation)
+ (Scan.repeat heading -- Parse.command_name theoryN --| Document_Source.annotation)
|-- Parse.!!! args;
fun read_tokens pos toks =