# HG changeset patch
# User wenzelm
# Date 1330265928 -3600
# Node ID b4bc54d4624b7e81accc44e26c117ba00cfe54b1
# Parent  f4ce220d2799bffe92564c7d38e01a072a175372
tuned signature;
clarified check;

diff -r f4ce220d2799 -r b4bc54d4624b src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sat Feb 25 15:33:36 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Feb 26 15:18:48 2012 +0100
@@ -23,7 +23,7 @@
   val USES = "uses"
   val BEGIN = "begin"
 
-  val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
+  private val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 
 
   /* theory file name */
@@ -38,7 +38,6 @@
     s match { case Thy_Name(name) => Some(name) case _ => None }
 
   def thy_path(path: Path): Path = path.ext("thy")
-  def thy_path(name: String): Path = Path.basic(name).ext("thy")
 
 
   /* header */
@@ -105,8 +104,8 @@
   {
     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)
+    val path = Path.explode(name)
+    if (name != name1) error("Bad file name " + thy_path(path) + " for theory " + quote(name1))
     header
   }
 }