# HG changeset patch
# User wenzelm
# Date 1313524446 -7200
# Node ID 4040d0ffac7b0500f900616feb8688eeb988e848
# Parent  cac52579f2c2d7d90fb49ec94732a23233011613
tuned message;

diff -r cac52579f2c2 -r 4040d0ffac7b 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 ""