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