1.1 --- a/src/Pure/Thy/thy_header.scala	Sat Feb 25 15:33:36 2012 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Feb 26 15:18:48 2012 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    val USES = "uses"
     1.5    val BEGIN = "begin"
     1.6  
     1.7 -  val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
     1.8 +  private val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
     1.9  
    1.10  
    1.11    /* theory file name */
    1.12 @@ -38,7 +38,6 @@
    1.13      s match { case Thy_Name(name) => Some(name) case _ => None }
    1.14  
    1.15    def thy_path(path: Path): Path = path.ext("thy")
    1.16 -  def thy_path(name: String): Path = Path.basic(name).ext("thy")
    1.17  
    1.18  
    1.19    /* header */
    1.20 @@ -105,8 +104,8 @@
    1.21    {
    1.22      val header = read(source)
    1.23      val name1 = header.name
    1.24 -    if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
    1.25 -    Path.explode(name)
    1.26 +    val path = Path.explode(name)
    1.27 +    if (name != name1) error("Bad file name " + thy_path(path) + " for theory " + quote(name1))
    1.28      header
    1.29    }
    1.30  }