clarified parser;

--- a/src/Pure/Thy/thy_header.scala	Sun Nov 29 16:11:52 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 29 16:21:27 2020 +0100
@@ -162,7 +162,7 @@
           { case None => Nil case Some(_ ~ xs) => xs }) ~
         (opt($$$(ABBREVS) ~! abbrevs) ^^
           { case None => Nil case Some(_ ~ xs) => xs }) ~
-        $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a._1, a._2, b, c, d).map(Symbol.decode) }
+        $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a._1, a._2, b, c, d) }
 
       val heading =
         (command(CHAPTER) |
@@ -225,7 +225,7 @@
       if (command) Token.Pos.command
       else (Token.Pos.file(node_name.node) /: skip_tokens)(_ advance _)
 
-    Parser.parse_header(tokens, pos).check(node_name)
+    Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
   }
 }