diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index f650e7f6a2..2c3d559d7d 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -114,7 +114,7 @@ parser::quote_scope::quote_scope(parser & p, bool q):
         m_p.m_in_quote = true;
         m_p.push_local_scope(false);
         m_p.m_quote_stack = cons(m_p.mk_parser_scope(), m_p.m_quote_stack);
-        m_p.clear_locals();
+        m_p.clear_expr_locals();
     } else {
         lean_assert(m_p.m_in_quote);
         lean_assert(m_p.m_quote_stack);
@@ -535,8 +535,7 @@ void parser::pop_local_scope() {
     m_parser_scope_stack = tail(m_parser_scope_stack);
 }
 
-void parser::clear_locals() {
-    m_local_level_decls = local_level_decls();
+void parser::clear_expr_locals() {
     m_local_decls       = local_expr_decls();
 }
 
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 8e29b39efe..b5a8cfec32 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -433,7 +433,7 @@ public:
 
     bool in_quote() const { return m_in_quote; }
 
-    void clear_locals();
+    void clear_expr_locals();
     bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); }
     void add_local_level(name const & n, level const & l, bool is_variable = false);
     void add_local_expr(name const & n, expr const & p, bool is_variable = false);
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index b9a9f32fb0..58e5d86833 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -344,14 +344,14 @@ expr parse_begin_end_core(parser & p, pos_info const & start_pos,
 
 expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {
     parser::local_scope _(p);
-    p.clear_locals();
+    p.clear_expr_locals();
     return parse_begin_end_core(p, pos, get_end_tk());
 }
 
 expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     p.next();
     parser::local_scope _(p);
-    p.clear_locals();
+    p.clear_expr_locals();
     auto tac_pos = p.pos();
     expr tac  = parse_tactic(p);
     expr type = mk_tactic_unit();