--- a/src/Pure/Thy/thy_syntax.scala Mon May 17 10:20:55 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon May 17 14:23:54 2010 +0200
@@ -22,13 +22,13 @@
}
}
- 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)
}