src/Pure/General/position.ML
changeset 69348 f0aef5e337a2
parent 68858 e1796b8ddbae
child 70498 de75eea6ffc8
--- a/src/Pure/General/position.ML	Tue Nov 27 16:20:08 2018 +0100
+++ b/src/Pure/General/position.ML	Tue Nov 27 16:22:12 2018 +0100
@@ -238,7 +238,7 @@
       | (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;