src/Pure/General/position.ML

         (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
       | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
       | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
       | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
   in
-    if null props then ""
+    if s2 = "" then ""
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   end;
 
 val here_list = implode o map here;