diff -r 74db756853d4 -r 28d4db6c6e79 src/Pure/Thy/thy_header.scala
--- 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 _ =>