src/Pure/Isar/parse.scala

 {
   /* parsing tokens */
 
   trait Parser extends Parsers
   {
-    type Elem = Outer_Lex.Token
+    type Elem = Token
 
     def filter_proper = true
 
     private def proper(in: Input): Input =
       if (in.atEnd || !in.first.is_ignored || !filter_proper) in

 
     def atom(s: String, pred: Elem => Boolean): Parser[String] =
       token(s, pred) ^^ (_.content)
 
     def keyword(name: String): Parser[String] =
-      atom(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
-        tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
+      atom(Token.Kind.KEYWORD.toString + " \"" + name + "\"",
+        tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
 
     def name: Parser[String] = atom("name declaration", _.is_name)
     def xname: Parser[String] = atom("name reference", _.is_xname)
     def text: Parser[String] = atom("text", _.is_text)
     def ML_source: Parser[String] = atom("ML source", _.is_text)
     def doc_source: Parser[String] = atom("document source", _.is_text)
     def path: Parser[String] = atom("file name/path specification", _.is_name)
 
     private def tag_name: Parser[String] =
       atom("tag name", tok =>
-          tok.kind == Outer_Lex.Token_Kind.IDENT ||
-          tok.kind == Outer_Lex.Token_Kind.STRING)
+          tok.kind == Token.Kind.IDENT ||
+          tok.kind == Token.Kind.STRING)
 
     def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
 
 
     /* wrappers */
 
-    def parse[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = p(in)
-    def parse_all[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = parse(phrase(p), in)
+    def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
+    def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = parse(phrase(p), in)
   }
 }