diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp
index 51a84b403..c9a82cbc9 100644
--- a/src/frontends/lean/lean_parser.cpp
+++ b/src/frontends/lean/lean_parser.cpp
@@ -1204,7 +1204,7 @@ class parser::imp {
         formatter fmt = m_frontend.get_state().get_formatter();
         options opts  = m_frontend.get_state().get_options();
         unsigned indent = get_pp_indent(opts);
-        format r = group(format{fmt(v), space(), colon(), nest(indent, compose(line(), fmt(t)))});
+        format r = group(format{fmt(v, opts), space(), colon(), nest(indent, compose(line(), fmt(t, opts)))});
         regular(m_frontend) << mk_pair(r, opts) << endl;
     }
 
diff --git a/tests/lean/coercion2.lean.expected.out b/tests/lean/coercion2.lean.expected.out
index eaa9eef66..824592e5c 100644
--- a/tests/lean/coercion2.lean.expected.out
+++ b/tests/lean/coercion2.lean.expected.out
@@ -22,8 +22,8 @@ g b (t2r a)
   Set: lean::pp::notation
 g (g a b) a
 h (h r s) r
-a ++ b ++ a : R
-r ++ s ++ r : S
+g (g a b) a : R
+h (h r s) r : S
   Set: lean::pp::coercion
 g (g (t2r a) b) (t2r a)
 h (h r s) r
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index 70325afcf..7f0b738a1 100644
--- a/tests/lean/tst4.lean.expected.out
+++ b/tests/lean/tst4.lean.expected.out
@@ -9,7 +9,7 @@ f::explicit N n1 n2
 f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
   Assumed: EqNice
 EqNice::explicit N n1 n2
-f n1 n2 : N
+f::explicit N n1 n2 : N
 Congr::explicit :
     Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A), (f = g) → (a = b) → ((f a) = (g b))
 f::explicit N n1 n2