1.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Jun 24 17:17:17 2013 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Jun 24 23:33:14 2013 +0200
     1.3 @@ -37,9 +37,6 @@
     1.4    val empty: Outer_Syntax = new Outer_Syntax()
     1.5  
     1.6    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
     1.7 -
     1.8 -  def init_pure(): Outer_Syntax =
     1.9 -    init() + ("theory", Keyword.THY_BEGIN) + ("ML_file", Keyword.THY_LOAD)
    1.10  }
    1.11  
    1.12  final class Outer_Syntax private(
    1.13 @@ -76,11 +73,11 @@
    1.14  
    1.15    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.16      (this /: keywords) {
    1.17 -      case (syntax, ((name, Some((kind, _)), replace))) =>
    1.18 +      case (syntax, (name, Some((kind, _)), replace)) =>
    1.19          syntax +
    1.20            (Symbol.decode(name), kind, replace) +
    1.21            (Symbol.encode(name), kind, replace)
    1.22 -      case (syntax, ((name, None, replace))) =>
    1.23 +      case (syntax, (name, None, replace)) =>
    1.24          syntax +
    1.25            (Symbol.decode(name), replace) +
    1.26            (Symbol.encode(name), replace)