# HG changeset patch
# User wenzelm
# Date 1289677742 -3600
# Node ID f814863f391806f9884d5c0bea67a59db12d5d85
# Parent  d5fb1f1a58570fd3a2bda80c3e05d0eaa96a3cf7
tuned message;

diff -r d5fb1f1a5857 -r f814863f3918 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sat Nov 13 20:20:05 2010 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sat Nov 13 20:49:02 2010 +0100
@@ -79,7 +79,7 @@
 
 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;