changeset 70134 | e69f00f4b897 |
parent 69891 | def3ec9cdb7e |
child 72747 | 5f9d66155081 |
--- a/src/Pure/Thy/thy_header.ML Thu Apr 11 21:33:21 2019 +0200 +++ b/src/Pure/Thy/thy_header.ML Fri Apr 12 17:09:21 2019 +0200 @@ -137,7 +137,7 @@ val keyword_spec = Parse.group (fn () => "outer syntax keyword specification") - (Parse.name -- opt_files -- Document_Source.tags); + (Parse.name -- opt_files -- Document_Source.old_tags); val keyword_decl = Scan.repeat1 Parse.string_position --