diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 2a95cf068..55dea6202 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -274,10 +274,23 @@ auto pretty_fn::pp_sort(expr const & e) -> result {
     }
 }
 
+optional<name> pretty_fn::is_aliased(name const & n) const {
+    if (auto it = is_expr_aliased(m_env, n)) {
+        // must check if we are not shadow by current namespace
+        for (name const & ns : get_namespaces(m_env)) {
+            if (!ns.is_anonymous() && m_env.find(ns + *it))
+                return optional<name>();
+        }
+        return it;
+    } else {
+        return optional<name>();
+    }
+}
+
 auto pretty_fn::pp_const(expr const & e) -> result {
     name n = const_name(e);
     if (!m_full_names) {
-        if (auto it = is_expr_aliased(m_env, n)) {
+        if (auto it = is_aliased(n)) {
             n = *it;
         } else {
             for (name const & ns : get_namespaces(m_env)) {
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index f4d52e7e8..7da3d9d59 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -54,6 +54,7 @@ private:
     bool is_implicit(expr const & f);
     bool is_prop(expr const & e);
     bool has_implicit_args(expr const & f);
+    optional<name> is_aliased(name const & n) const;
 
     format pp_binder_block(buffer<name> const & names, expr const & type, binder_info const & bi);
     format pp_binders(buffer<expr> const & locals);
diff --git a/tests/lean/alias2.lean b/tests/lean/alias2.lean
new file mode 100644
index 000000000..c763cad56
--- /dev/null
+++ b/tests/lean/alias2.lean
@@ -0,0 +1,11 @@
+import logic
+
+namespace foo
+   definition t := true
+end foo
+open foo
+
+namespace bla
+  definition t := false
+  check foo.t   -- <<< must print foo.t : Prop instead of t : Prop
+end bla
diff --git a/tests/lean/alias2.lean.expected.out b/tests/lean/alias2.lean.expected.out
new file mode 100644
index 000000000..d89d0ce7c
--- /dev/null
+++ b/tests/lean/alias2.lean.expected.out
@@ -0,0 +1 @@
+foo.t : Prop