diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 9fae95a935..c9534872cd 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -212,6 +212,11 @@ void parser::scan() {
     check_break_before();
     check_break_at_pos();
     pos_info curr_pos = pos();
+    if (m_error_since_last_cmd && (curr_is_command() && !curr_is_token(get_end_tk()))) {
+        // If we're during error recovery, do not read past command tokens.
+        // `end` is not treated as a command token since it occurs in begin-end blocks.
+        return;
+    }
     if (m_break_at_pos && m_break_at_pos->first == curr_pos.first && curr_is_identifier()) {
         name curr_ident = get_name_val();
         m_curr = m_scanner.scan(m_env);
@@ -353,10 +358,13 @@ bool parser::curr_is_token_or_id(name const & tk) const {
         return false;
 }
 
-void parser::check_token_next(name const & tk, char const * msg) {
-    if (!curr_is_token(tk))
-        return maybe_throw_error({msg, pos()});
+bool parser::check_token_next(name const & tk, char const * msg) {
+    if (!curr_is_token(tk)) {
+        maybe_throw_error({msg, pos()});
+        return false;
+    }
     next();
+    return true;
 }
 
 void parser::check_token_or_id_next(name const & tk, char const * msg) {
@@ -2451,6 +2459,7 @@ void parser::get_imports(std::vector<module_name> & imports) {
 
 bool parser::parse_command_like() {
     init_scanner();
+    m_error_since_last_cmd = false;
 
     // We disable hash-consing while parsing to make sure the pos-info are correct.
     scoped_expr_caching disable(false);
@@ -2559,6 +2568,7 @@ void parser::maybe_throw_error(parser_error && err) {
             check_system("parser error recovery");
             mk_message(ERROR).set_exception(err).report();
             m_last_recovered_error_pos = err_pos;
+            m_error_since_last_cmd = true;
         }
     } else {
         throw err;
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index c5e1cb6bd3..3f2105a6b5 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -70,6 +70,7 @@ class parser : public abstract_parser {
 
     // error recovery
     bool                   m_error_recovery = true;
+    bool                   m_error_since_last_cmd = false;
     pos_info               m_last_recovered_error_pos {0, 0};
 
     // curr command token
@@ -273,8 +274,8 @@ public:
     virtual void next() override final { if (m_curr != token_kind::Eof) scan(); }
     /** \brief Return true iff the current token is a keyword (or command keyword) named \c tk */
     virtual bool curr_is_token(name const & tk) const override final;
-    /** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */
-    void check_token_next(name const & tk, char const * msg);
+    /** \brief Check current token, and move to next characther, throw exception if current token is not \c tk.  Returns true if succesful. */
+    bool check_token_next(name const & tk, char const * msg);
     void check_token_or_id_next(name const & tk, char const * msg);
     /** \brief Check if the current token is an identifier, if it is return it and move to next token,
         otherwise throw an exception. */
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index 322f686d90..e6e359857d 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -421,6 +421,17 @@ struct parse_begin_end_block_fn {
     }
 
     expr operator()(pos_info const & start_pos, name const & end_token) {
+        auto sync = [&] {
+            while (!m_p.curr_is_token(get_comma_tk()) && !m_p.curr_is_token(end_token) &&
+                    !m_p.curr_is_token(get_semicolon_tk()) && !m_p.curr_is_token(get_orelse_tk())) {
+                auto pos0 = m_p.pos();
+                m_p.next();
+                if (m_p.pos() == pos0) break;
+            }
+            if (!m_p.curr_is_token(get_end_tk())) m_p.next();
+            m_p.maybe_throw_error({"sync", m_p.pos()});
+        };
+
         m_p.next();
         name new_tac_class = m_tac_class;
         if (m_tac_class == get_tactic_name())
@@ -435,30 +446,24 @@ struct parse_begin_end_block_fn {
         m_tac_class = new_tac_class;
         buffer<expr> to_concat;
         to_concat.push_back(mk_tactic_save_info(m_p, start_pos, m_tac_class));
-        try {
-            while (!m_p.curr_is_token(end_token)) {
-                pos_info pos = m_p.pos();
-                try {
-                    to_concat.push_back(parse_tactic());
-                    if (!m_p.curr_is_token(end_token)) {
-                        m_p.without_break_at_pos<void>([&]() {
-                            m_p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
-                        });
-                    }
-                    to_concat.push_back(mk_save_info());
-                } catch (break_at_pos_exception & ex) {
-                    ex.report_goal_pos(pos);
-                    throw;
-                }
-                if (m_p.pos() == pos) { // unsuccessful error recovery
-                    consume_until_end_or_command(m_p);
-                    break;
+        while (!m_p.curr_is_token(end_token)) {
+            pos_info pos = m_p.pos();
+            try {
+                to_concat.push_back(parse_tactic());
+                if (!m_p.curr_is_token(end_token)) {
+                    m_p.without_break_at_pos<void>([&]() {
+                        if (!m_p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected")) {
+                            sync();
+                        }
+                    });
                 }
+                to_concat.push_back(mk_save_info());
+            } catch (break_at_pos_exception & ex) {
+                ex.report_goal_pos(pos);
+                throw;
             }
-        } catch (exception & ex) {
-            if (end_token == get_end_tk())
-                consume_until_end_or_command(m_p);
-            throw;
+            if (m_p.pos() == pos) sync();
+            if (m_p.pos() == pos) break;
         }
         auto end_pos = m_p.pos();
         expr r = concat(to_concat, start_pos);