diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 68f85c34a2..9376e4b7dd 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3635,7 +3635,7 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
                       if (expected_type) tout() << "expected type:\n" << instantiate_mvars(*expected_type) << "\n";);
     expr e2 = recover_expr_from_exception(expected_type, e, [&] () -> expr {
         if (auto p = get_pos(e)) {
-            m_last_pos = p;
+            flet<optional<pos_info>> _(m_last_pos, p);
             return visit(unwrap_pos(e), expected_type);
         } else if (is_placeholder(e)) {
             return visit_placeholder(e, expected_type);