diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 1afa640b4..4b74868ef 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -612,6 +612,8 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
     } else if (is_placeholder(p)) {
         return true;
     } else if (is_constant(p) && is_constant(e)) {
+        if (const_name(p) != const_name(e))
+            return false;
         levels p_ls = const_levels(p);
         levels e_ls = const_levels(p);
         while (!is_nil(p_ls)) {
diff --git a/tests/lean/notation6.lean b/tests/lean/notation6.lean
new file mode 100644
index 000000000..bd1eea649
--- /dev/null
+++ b/tests/lean/notation6.lean
@@ -0,0 +1,9 @@
+import logic data.num
+open num
+notation `o` := 10
+check 11
+constant f : num → num
+check o + 1
+check f o + o + o
+eval 9 + 1
+eval o+4
diff --git a/tests/lean/notation6.lean.expected.out b/tests/lean/notation6.lean.expected.out
new file mode 100644
index 000000000..84a39dc83
--- /dev/null
+++ b/tests/lean/notation6.lean.expected.out
@@ -0,0 +1,5 @@
+11 : num
+o + 1 : num
+f o + o + o : num
+o
+14