tuned message;
authorwenzelm
Tue, 16 Aug 2011 21:54:06 +0200
changeset 44224 4040d0ffac7b
parent 44223 cac52579f2c2
child 44225 a8f921e6484f
tuned message;
src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 16 21:50:53 2011 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 16 21:54:06 2011 +0200
@@ -171,7 +171,7 @@
       (case (line_of pos, file_of pos) of
         (SOME i, NONE) => "(line " ^ string_of_int i ^ ")"
       | (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")"
-      | (NONE, SOME name) => "(" ^ quote name ^ ")"
+      | (NONE, SOME name) => "(file " ^ quote name ^ ")"
       | _ => "");
   in
     if null props then ""