src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Tue Jul 05 21:53:59 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Jul 05 22:38:44 2011 +0200
@@ -112,7 +112,8 @@
   {
     val header = read(source)
     val name1 = header.name
-    if (name == name1) header
-    else error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
+    if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
+    Path.explode(name)
+    header
   }
 }