src/Pure/Thy/thy_header.ML
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 --