diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp
index 0f640b6688..5d652eb2f6 100644
--- a/src/kernel/justification.cpp
+++ b/src/kernel/justification.cpp
@@ -317,8 +317,11 @@ justification mk_justification(optional<expr> const & s, pp_jst_fn const & fn) {
     return justification(new (get_asserted_allocator().allocate()) asserted_cell(fn, s));
 }
 justification mk_justification(optional<expr> const & s, pp_jst_sfn const & fn) {
-    return mk_justification(s, [=](formatter const & fmt, pos_info_provider const * p, substitution const & subst) {
-            return compose(to_pos(s, p), fn(fmt, subst)); });
+    return mk_justification(s, [=](formatter const & fmt, pos_info_provider const *, substitution const & subst) {
+            // Remark: we are not using to_pos(s, p) anymore because we don't try to display complicated error messages anymore.
+            // return compose(to_pos(s, p), fn(fmt, subst));
+            return fn(fmt, subst);
+        });
 }
 justification mk_justification(char const * msg, optional<expr> const & s) {
     std::string _msg(msg);
diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out
index 9cc3bc9188..41aed30d71 100644
--- a/tests/lean/empty.lean.expected.out
+++ b/tests/lean/empty.lean.expected.out
@@ -1,2 +1,2 @@
-empty.lean:5:25: error: empty.lean:5:25: failed to synthesize placeholder
+empty.lean:5:25: error: failed to synthesize placeholder
  ⊢ inhabited Empty