diff -r 4a9f76263ece -r 76979adf0b96 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Feb 17 20:54:03 2014 +0100
+++ b/src/Pure/General/position.ML	Mon Feb 17 21:37:41 2014 +0100
@@ -192,7 +192,7 @@
         (SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")"
       | (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")"
       | (NONE, SOME name) => "(file " ^ quote name ^ ")"
-      | _ => "");
+      | _ => if is_reported pos then "\\<here>" else "");
   in
     if null props then ""
     else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s