# HG changeset patch
# User wenzelm
# Date 1606663287 -3600
# Node ID 1cc74982d03882e58f42938d838c3b4883e8b349
# Parent  83e581c9a5f1f8be3c2a468bc65052c6633c36b7
clarified parser;

diff -r 83e581c9a5f1 -r 1cc74982d038 src/Pure/Thy/thy_header.scala
--- 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)
   }
 }