src/Pure/Thy/thy_syntax.scala
changeset 36956 21be4832c362
parent 36948 d2cdad45fd14
child 38239 89a4d1028fb3
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon May 17 10:20:55 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon May 17 14:23:54 2010 +0200
     1.3 @@ -22,13 +22,13 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  type Span = List[Outer_Lex.Token]
     1.8 +  type Span = List[Token]
     1.9  
    1.10 -  def parse_spans(toks: List[Outer_Lex.Token]): List[Span] =
    1.11 +  def parse_spans(toks: List[Token]): List[Span] =
    1.12    {
    1.13      import parser._
    1.14  
    1.15 -    parse(rep(command_span), Outer_Lex.reader(toks)) match {
    1.16 +    parse(rep(command_span), Token.reader(toks)) match {
    1.17        case Success(spans, rest) if rest.atEnd => spans
    1.18        case bad => error(bad.toString)
    1.19      }