src/Pure/Thy/thy_header.ML

     (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
   | _ => error ("Bad theory file specification: " ^ Path.implode path));
 
 fun consistent_name name name' =
   if name = name' then ()
-  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
-    " does not agree with theory name " ^ quote name');
+  else error ("Bad file name " ^ quote (Path.implode (thy_path name)) ^
+    " for theory " ^ quote name');
 
 end;