diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index c2f54290a..d433efa39 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -832,7 +832,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
         }
         r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
     }
-    if (m_no_undef_id_error)
+    if (!r && m_no_undef_id_error)
         r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
     if (!r)
         throw parser_error(sstream() << "unknown identifier '" << id << "'", p);