diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp
index fbc061569..88e524ba7 100644
--- a/src/kernel/formatter.cpp
+++ b/src/kernel/formatter.cpp
@@ -44,7 +44,7 @@ pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
     if (is_internal_name(n))
         n = g_x;
     n = pick_unused_name(binding_body(b), n);
-    expr c = mk_local(n, preserve_type ? binding_domain(b) : expr());
+    expr c = mk_local(n, preserve_type ? binding_domain(b) : expr(), binding_info(b));
     return mk_pair(instantiate(binding_body(b), c), c);
 }
 
diff --git a/tests/lean/pp.lean b/tests/lean/pp.lean
new file mode 100644
index 000000000..500b9d49d
--- /dev/null
+++ b/tests/lean/pp.lean
@@ -0,0 +1,7 @@
+check λ {A : Type.{1}} (B : Type.{1}) (a : A) (b : B), a
+check λ {A : Type.{1}} {B : Type.{1}} (a : A) (b : B), a
+check λ (A : Type.{1}) {B : Type.{1}} (a : A) (b : B), a
+check λ (A : Type.{1}) (B : Type.{1}) (a : A) (b : B), a
+check λ [A : Type.{1}] (B : Type.{1}) (a : A) (b : B), a
+check λ {{A : Type.{1}}} {B : Type.{1}} (a : A) (b : B), a
+check λ {{A : Type.{1}}} {{B : Type.{1}}} (a : A) (b : B), a
diff --git a/tests/lean/pp.lean.expected.out b/tests/lean/pp.lean.expected.out
new file mode 100644
index 000000000..be3384c8e
--- /dev/null
+++ b/tests/lean/pp.lean.expected.out
@@ -0,0 +1,7 @@
+λ {A : Type} (B : Type) (a : A) (b : B), a : Π {A : Type} (B : Type), A → B → A
+λ {A B : Type} (a : A) (b : B), a : Π {A B : Type}, A → B → A
+λ (A : Type) {B : Type} (a : A) (b : B), a : Π (A : Type) {B : Type}, A → B → A
+λ (A B : Type) (a : A) (b : B), a : Π (A B : Type), A → B → A
+λ [A : Type] (B : Type) (a : A) (b : B), a : Π [A : Type] (B : Type), A → B → A
+λ ⦃A : Type⦄ {B : Type} (a : A) (b : B), a : Π ⦃A : Type⦄ {B : Type}, A → B → A
+λ ⦃A B : Type⦄ (a : A) (b : B), a : Π ⦃A B : Type⦄, A → B → A
diff --git a/tests/lean/t7.lean.expected.out b/tests/lean/t7.lean.expected.out
index 022fc6d0b..308042071 100644
--- a/tests/lean/t7.lean.expected.out
+++ b/tests/lean/t7.lean.expected.out
@@ -2,5 +2,5 @@ id : ?M_1 → ?M_1
 trans : (?M_1 → ?M_1 → Prop) → Prop
 symm : (?M_1 → ?M_1 → Prop) → Prop
 equivalence : (?M_1 → ?M_1 → Prop) → Prop
-λ (A : Type) (R : A → A → Prop),
+λ {A : Type} (R : A → A → Prop),
   and (and (refl R) (symm R)) (trans R)