tuned;

--- a/src/Pure/PIDE/resources.scala	Thu Sep 28 15:11:32 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri Sep 29 17:03:33 2017 +0200
@@ -127,7 +127,7 @@
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
-        val header = Thy_Header.read(reader, start, strict).decode_symbols
+        val header = Thy_Header.read(reader, start, strict)
 
         val base_name = node_name.theory_base_name
         val (name, pos) = header.name

--- a/src/Pure/Thy/thy_header.scala	Thu Sep 28 15:11:32 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Sep 29 17:03:33 2017 +0200
@@ -138,7 +138,14 @@
       (opt($$$(ABBREVS) ~! abbrevs) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
       $$$(BEGIN) ^^
-      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
+      { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ =>
+          val f = Symbol.decode _
+          Thy_Header((f(name), pos),
+            imports.map({ case (a, b) => (f(a), b) }),
+            keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
+              (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
+            abbrevs.map({ case (a, b) => (f(a), f(b)) }))
+      }
 
     val heading =
       (command(CHAPTER) |
@@ -197,20 +204,8 @@
   }
 }
 
-
 sealed case class Thy_Header(
   name: (String, Position.T),
   imports: List[(String, Position.T)],
   keywords: Thy_Header.Keywords,
   abbrevs: Thy_Header.Abbrevs)
-{
-  def decode_symbols: Thy_Header =
-  {
-    val f = Symbol.decode _
-    Thy_Header((f(name._1), name._2),
-      imports.map({ case (a, b) => (f(a), b) }),
-      keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
-        (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
-      abbrevs.map({ case (a, b) => (f(a), f(b)) }))
-  }
-}