--- a/src/Pure/General/position.ML Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/General/position.ML Sun Mar 06 16:19:02 2016 +0100
@@ -208,7 +208,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 ("", ""));
+ | _ => if is_reported pos then ("", "\<here>") else ("", ""));
in
if null props then ""
else s1 ^ Markup.markup (Markup.properties props Markup.position) s2