src/Pure/Thy/thy_header.scala

   val USES = "uses"
   val BEGIN = "begin"
 
   val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 
-  sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
-  {
-    def map(f: String => String): Header =
-      Header(f(name), imports.map(f), uses.map(f))
-  }
-
 
   /* file name */
 
   def thy_path(name: String): Path = Path.basic(name).ext("thy")
 

     }
 
 
   /* header */
 
-  val header: Parser[Header] =
+  val header: Parser[Thy_Header] =
   {
     val file_name = atom("file name", _.is_name)
     val theory_name = atom("theory name", _.is_name)
 
     val file =

 
     val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }
 
     val args =
       theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
-        { case x ~ (_ ~ (ys ~ zs ~ _)) => Header(x, ys, zs) }
+        { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) }
 
     (keyword(HEADER) ~ tags) ~!
       ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
     (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   }
 
 
   /* read -- lazy scanning */
 
-  def read(reader: Reader[Char]): Header =
+  def read(reader: Reader[Char]): Thy_Header =
   {
     val token = lexicon.token(_ => false)
     val toks = new mutable.ListBuffer[Token]
 
     @tailrec def scan_to_begin(in: Reader[Char])

       case Success(result, _) => result
       case bad => error(bad.toString)
     }
   }
 
-  def read(source: CharSequence): Header =
+  def read(source: CharSequence): Thy_Header =
     read(new CharSequenceReader(source))
 
-  def read(file: File): Header =
+  def read(file: File): Thy_Header =
   {
     val reader = Scan.byte_reader(file)
     try { read(reader).map(Standard_System.decode_permissive_utf8) }
     finally { reader.close }
   }
 
 
   /* check */
 
-  def check(name: String, source: CharSequence): Header =
+  def check(name: String, source: CharSequence): Thy_Header =
   {
     val header = read(source)
     val name1 = header.name
     if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
     Path.explode(name)
     header
   }
 }
+
+
+sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String])
+{
+  def map(f: String => String): Thy_Header =
+    Thy_Header(f(name), imports.map(f), uses.map(f))
+}
+