src/Pure/Thy/thy_header.scala
changeset 72773 93b50b9e3494
parent 72765 f34f5c057c9e
child 72774 51c0f79d6eed
--- a/src/Pure/Thy/thy_header.scala	Sun Nov 29 14:57:15 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:23:18 2020 +0100
@@ -221,7 +221,7 @@
     val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
     val pos = (start /: drop_tokens)(_.advance(_))
 
-    Parser.parse_header(tokens, pos)
+    Parser.parse_header(tokens, pos).check_keywords
   }
 }