src/Pure/Isar/outer_syntax.scala
changeset 52439 4cf3f6153eb8
parent 52066 83b7b88770c9
child 53280 c63a016805b9
--- a/src/Pure/Isar/outer_syntax.scala	Mon Jun 24 17:17:17 2013 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Mon Jun 24 23:33:14 2013 +0200
@@ -37,9 +37,6 @@
   val empty: Outer_Syntax = new Outer_Syntax()
 
   def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
-
-  def init_pure(): Outer_Syntax =
-    init() + ("theory", Keyword.THY_BEGIN) + ("ML_file", Keyword.THY_LOAD)
 }
 
 final class Outer_Syntax private(
@@ -76,11 +73,11 @@
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
     (this /: keywords) {
-      case (syntax, ((name, Some((kind, _)), replace))) =>
+      case (syntax, (name, Some((kind, _)), replace)) =>
         syntax +
           (Symbol.decode(name), kind, replace) +
           (Symbol.encode(name), kind, replace)
-      case (syntax, ((name, None, replace))) =>
+      case (syntax, (name, None, replace)) =>
         syntax +
           (Symbol.decode(name), replace) +
           (Symbol.encode(name), replace)