simplified class Thy_Header;

--- a/src/Pure/PIDE/document.scala	Fri Aug 12 11:41:26 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 12 12:03:17 2011 +0200
@@ -51,7 +51,7 @@
     case class Edits[A](edits: List[A]) extends Edit[A]
     case class Update_Header[A](header: Header) extends Edit[A]
 
-    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
+    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header])
     val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
 
     val empty: Node = Node(empty_header, Map(), Linear_Set())

--- a/src/Pure/PIDE/isar_document.scala	Fri Aug 12 11:41:26 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 12 12:03:17 2011 +0200
@@ -150,7 +150,7 @@
             { case Document.Node.Remove() => (Nil, Nil) },
             { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
             { case Document.Node.Update_Header(
-                  Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) =>
+                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
                 (Nil, triple(string, list(string), list(string))(a, b, c)) },
             { case Document.Node.Update_Header(
                   Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))

--- a/src/Pure/System/session.scala	Fri Aug 12 11:41:26 2011 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 12 12:03:17 2011 +0200
@@ -146,7 +146,7 @@
     override def is_loaded(name: String): Boolean =
       loaded_theories.contains(name)
 
-    override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
+    override def check_thy(dir: Path, name: String): (String, Thy_Header) =
     {
       val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))

--- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 11:41:26 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 12:03:17 2011 +0200
@@ -25,12 +25,6 @@
 
   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 */
 
@@ -45,7 +39,7 @@
 
   /* 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)
@@ -57,7 +51,7 @@
 
     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 } |
@@ -67,7 +61,7 @@
 
   /* 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]
@@ -89,10 +83,10 @@
     }
   }
 
-  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) }
@@ -102,7 +96,7 @@
 
   /* check */
 
-  def check(name: String, source: CharSequence): Header =
+  def check(name: String, source: CharSequence): Thy_Header =
   {
     val header = read(source)
     val name1 = header.name
@@ -111,3 +105,11 @@
     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))
+}
+

--- a/src/Pure/Thy/thy_info.scala	Fri Aug 12 11:41:26 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Fri Aug 12 12:03:17 2011 +0200
@@ -38,7 +38,7 @@
 
   /* dependencies */
 
-  type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
+  type Deps = Map[String, Exn.Result[(String, Thy_Header)]]  // name -> (text, header)
 
   private def require_thys(ignored: String => Boolean,
       initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =

--- a/src/Pure/Thy/thy_load.scala	Fri Aug 12 11:41:26 2011 +0200
+++ b/src/Pure/Thy/thy_load.scala	Fri Aug 12 12:03:17 2011 +0200
@@ -10,6 +10,6 @@
 {
   def is_loaded(name: String): Boolean
 
-  def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
+  def check_thy(dir: Path, name: String): (String, Thy_Header)
 }