diff -r de848ac5e0d7 -r 089f2edefb77 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Apr 04 22:16:42 2017 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Apr 04 22:53:01 2017 +0200
@@ -57,9 +57,9 @@
 
   /* keywords */
 
-  def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
+  def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
   {
-    val keywords1 = keywords + (name, kind, tags)
+    val keywords1 = keywords + (name, kind, exts)
     val completion1 =
       completion.add_keyword(name).
         add_abbrevs(
@@ -71,8 +71,8 @@
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
     (this /: keywords) {
-      case (syntax, (name, ((kind, tags), _))) =>
-        syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
+      case (syntax, (name, ((kind, exts), _))) =>
+        syntax + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
     }