author | wenzelm |
Tue, 05 Jul 2011 22:38:44 +0200 | |
changeset 44547 | e9f26e66692d |
parent 44546 | a250b092ac66 |
child 44548 | 29eb1cd29961 |
1.1 --- a/src/Pure/Thy/thy_header.scala Tue Jul 05 21:53:59 2011 +0200 1.2 +++ b/src/Pure/Thy/thy_header.scala Tue Jul 05 22:38:44 2011 +0200 1.3 @@ -112,7 +112,8 @@ 1.4 { 1.5 val header = read(source) 1.6 val name1 = header.name 1.7 - if (name == name1) header 1.8 - else error("Bad file name " + thy_path(name) + " for theory " + quote(name1)) 1.9 + if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1)) 1.10 + Path.explode(name) 1.11 + header 1.12 } 1.13 }