src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Nov 05 20:20:57 2014 +0100
@@ -27,7 +27,7 @@
   val AND = "and"
   val BEGIN = "begin"
 
-  private val keywords =
+  private val header_keywords =
     Keyword.Keywords(
       List("%", "(", ")", ",", "::", "==", AND, BEGIN,
         HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY))
@@ -96,7 +96,7 @@
 
   def read(reader: Reader[Char]): Thy_Header =
   {
-    val token = Token.Parsers.token(keywords)
+    val token = Token.Parsers.token(header_keywords)
     val toks = new mutable.ListBuffer[Token]
 
     @tailrec def scan_to_begin(in: Reader[Char])