diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 99936ec4e..fb1ba1358 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1542,7 +1542,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
             new_as.push_back(*r);
         bool has_constructor = false;
         for (auto const & e : as) {
-            has_constructor |= (bool)inductive::is_intro_rule(m_env, e);
+            has_constructor |= static_cast<bool>(inductive::is_intro_rule(m_env, e));
             new_as.push_back(copy_with_new_pos(mk_constant(e, ls), p));
         }
         if (m_undef_id_behavior == undef_id_behavior::AssumeLocalAndAlsoDefinedNonConstructors &&
diff --git a/tests/lean/630.lean.expected.out b/tests/lean/630.lean.expected.out
index df473450f..3616637ad 100644
--- a/tests/lean/630.lean.expected.out
+++ b/tests/lean/630.lean.expected.out
@@ -1,4 +1,4 @@
-definition pnat.pnat : Type₁ :=
+definition pnat : Type₁ :=
 {n | n > 0}
 inductive prod : Type → Type → Type
 constructors:
diff --git a/tests/lean/run/eq2.lean b/tests/lean/run/eq2.lean
index 6ebf0d1cd..103496952 100644
--- a/tests/lean/run/eq2.lean
+++ b/tests/lean/run/eq2.lean
@@ -1,5 +1,5 @@
 definition symm {A : Type} : Π {a b : A}, a = b → b = a
-| a a rfl := rfl
+| a a (eq.refl a) := rfl
 
 definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
-| a a a rfl rfl := rfl
+| a a a (eq.refl a) (eq.refl a) := rfl
diff --git a/tests/lean/run/match_tac.lean b/tests/lean/run/match_tac.lean
index e16ce6837..d8443a538 100644
--- a/tests/lean/run/match_tac.lean
+++ b/tests/lean/run/match_tac.lean
@@ -16,4 +16,4 @@ end
 open nat
 
 example : ∀ (a b : nat), a = b → b = a
-| a a rfl := rfl
+| a a (eq.refl a) := rfl