src/Pure/Syntax/lexicon.ML

--- a/src/Pure/Syntax/lexicon.ML	Thu Feb 20 17:21:48 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Thu Feb 20 17:51:16 2014 +0100
@@ -290,7 +290,9 @@
         (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
       (toks, []) => toks
     | (_, ss) =>
-        error (err_prefix ^ Symbol_Pos.content ss ^ Position.here (#1 (Symbol_Pos.range ss))))
+        error ("Inner lexical error" ^ Position.here (#1 (Symbol_Pos.range ss)) ^
+          Markup.markup Markup.no_report ("\nat " ^ quote (Symbol_Pos.content ss))))
+
   end;