| changeset 51627 | 589daaf48dba |
| parent 51294 | 0850d43cb355 |
| child 53962 | 65bca53daf70 |
--- a/src/Pure/Thy/thy_header.ML Fri Apr 05 20:43:43 2013 +0200 +++ b/src/Pure/Thy/thy_header.ML Fri Apr 05 20:54:55 2013 +0200 @@ -118,7 +118,7 @@ val header = (Parse.command_name headerN -- Parse.tags) |-- - (Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon -- + (Parse.!!! (Parse.document_source -- Scan.repeat Parse.semicolon -- (Parse.command_name theoryN -- Parse.tags) |-- args)) || (Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;