--- a/src/Pure/Thy/thy_header.scala Fri Feb 14 14:52:50 2014 +0100
+++ b/src/Pure/Thy/thy_header.scala Fri Feb 14 15:42:27 2014 +0100
@@ -82,13 +82,13 @@
def read(reader: Reader[Char]): Thy_Header =
{
- val token = lexicon.token(_ => false)
+ val token = Scan.Parsers.token(lexicon, _ => false)
val toks = new mutable.ListBuffer[Token]
@tailrec def scan_to_begin(in: Reader[Char])
{
token(in) match {
- case lexicon.Success(tok, rest) =>
+ case Scan.Parsers.Success(tok, rest) =>
toks += tok
if (!tok.is_begin) scan_to_begin(rest)
case _ =>