author | wenzelm |
Tue, 05 Jul 2011 22:38:44 +0200 | |
changeset 43672 | e9f26e66692d |
parent 43671 | a250b092ac66 |
child 43673 | 29eb1cd29961 |
--- 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 } }