# HG changeset patch
# User wenzelm
# Date 1344699780 -7200
# Node ID 85eeb06ec1c442ecdbf56631b90afdf160ce4910
# Parent  e3b7087bb923d66914864c497a31b9a2775bda37
tuned markup;

diff -r e3b7087bb923 -r 85eeb06ec1c4 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sat Aug 11 17:40:33 2012 +0200
+++ b/src/Pure/General/symbol_pos.ML	Sat Aug 11 17:43:00 2012 +0200
@@ -70,7 +70,8 @@
       | get_pos ((_, pos) :: _) = Position.str_of pos;
 
     fun err (syms, msg) = fn () =>
-      text () ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^
+      text () ^ get_pos syms ^
+      Markup.markup Isabelle_Markup.no_report (" at " ^ Symbol.beginning 10 (map symbol syms)) ^
       (case msg of NONE => "" | SOME m => "\n" ^ m ());
   in Scan.!! err scan end;