src/Pure/Isar/keyword.scala

   val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
   val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
   val qed_global = Set(QED_GLOBAL)
 
 
-  type Spec = ((String, List[String]), List[String])
-
-
 
   /** keyword tables **/
+
+  type Spec = ((String, List[String]), List[String])
 
   object Keywords
   {
     def empty: Keywords = new Keywords()
   }

 
     /* add keywords */
 
     def + (name: String): Keywords = new Keywords(minor + name, major, commands)
     def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
-    def + (name: String, kind: (String, List[String])): Keywords =
+    def + (name: String, kind_tags: (String, List[String])): Keywords =
     {
       val major1 = major + name
-      val commands1 = commands + (name -> kind)
+      val commands1 = commands + (name -> kind_tags)
       new Keywords(minor, major1, commands1)
     }
+
+    def add_keywords(header: Thy_Header.Keywords): Keywords =
+      (this /: header) {
+        case (keywords, (name, None, _)) =>
+          keywords + Symbol.decode(name) + Symbol.encode(name)
+        case (keywords, (name, Some((kind_tags, _)), _)) =>
+          keywords + (Symbol.decode(name), kind_tags) + (Symbol.encode(name), kind_tags)
+      }
 
 
     /* command kind */
 
     def command_kind(name: String): Option[String] = commands.get(name).map(_._1)