# HG changeset patch
# User wenzelm
# Date 1309898324 -7200
# Node ID e9f26e66692d5c03d2606898a520a1168f263f5e
# Parent  a250b092ac660a33b09a0a1c5c3cbeac48fdfb6e
theory name needs to conform to Path syntax;

diff -r a250b092ac66 -r e9f26e66692d 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
   }
 }