src/Pure/Thy/thy_syntax.scala

       val body = not(rep(whitespace) ~ (command | eof)) ~> not_eof
       command ~ rep(body) ^^ { case x ~ ys => x :: ys } | rep1(whitespace) | rep1(body)
     }
   }
 
-  type Span = List[Outer_Lex.Token]
+  type Span = List[Token]
 
-  def parse_spans(toks: List[Outer_Lex.Token]): List[Span] =
+  def parse_spans(toks: List[Token]): List[Span] =
   {
     import parser._
 
-    parse(rep(command_span), Outer_Lex.reader(toks)) match {
+    parse(rep(command_span), Token.reader(toks)) match {
       case Success(spans, rest) if rest.atEnd => spans
       case bad => error(bad.toString)
     }
   }
 }