src/Pure/Isar/keyword.scala

--- a/src/Pure/Isar/keyword.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/Isar/keyword.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -163,7 +163,7 @@
 
     def add_keywords(header: Thy_Header.Keywords): Keywords =
       (this /: header) {
-        case (keywords, (name, ((kind, exts), _), _)) =>
+        case (keywords, (name, ((kind, exts), _))) =>
           if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
           else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
       }