diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 692c87ce7..03cc0cf55 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -521,7 +521,7 @@ static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &
 static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_info const &) {
     name n = p.check_id_next("invalid '#' local notation, identifier expected");
     environment env = overwrite_notation(p.env(), n);
-    return p.parse_scoped_expr(0, nullptr, env);
+    return p.parse_expr_with_env(env);
 }
 
 static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index c1a503ad0..51cd38985 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1348,6 +1348,11 @@ expr parser::parse_scoped_expr(unsigned num_ps, expr const * ps, local_environme
     return parse_expr(rbp);
 }
 
+expr parser::parse_expr_with_env(local_environment const & lenv, unsigned rbp) {
+    flet<environment> set_env(m_env, lenv);
+    return parse_expr(rbp);
+}
+
 static bool is_tactic_type(expr const & e) {
     return is_constant(e) && const_name(e) == get_tactic_name();
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 257e58b14..24ac2cce3 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -402,6 +402,7 @@ public:
         return parse_scoped_expr(num_params, ps, local_environment(m_env), rbp);
     }
     expr parse_scoped_expr(buffer<expr> const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
+    expr parse_expr_with_env(local_environment const & lenv, unsigned rbp = 0);
 
     expr parse_tactic(unsigned rbp = 0);
     expr parse_tactic_expr_arg(unsigned rbp = 0);
diff --git a/tests/lean/run/override_on_equations.lean b/tests/lean/run/override_on_equations.lean
new file mode 100644
index 000000000..1f1e5241d
--- /dev/null
+++ b/tests/lean/run/override_on_equations.lean
@@ -0,0 +1,24 @@
+open nat
+
+inductive expr :=
+| zero : expr
+| one  : expr
+| add  : expr → expr → expr
+
+namespace expr
+
+infix `+` := expr.add
+
+set_option pp.notation false
+
+definition ev : expr → nat
+| zero          := 0
+| one           := 1
+| #expr (a + b) := ev a + ev b
+
+definition foo : expr := add zero (add one one)
+
+example : ev foo = 2 :=
+rfl
+
+end expr