diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index e816ab270..9c97a47c3 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -354,7 +354,7 @@ pair<expr, constraint_seq> type_checker::check(expr const & e, level_param_names
     return infer_type_core(e, false);
 }
 
-pair<expr, constraint_seq> type_checker::check_ignore_levels(expr const & e) {
+pair<expr, constraint_seq> type_checker::check_ignore_undefined_universes(expr const & e) {
     flet<level_param_names const *> updt(m_params, nullptr);
     return infer_type_core(e, false);
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 0da64341d..16dac8c4e 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -148,8 +148,8 @@ public:
        The result is meaningful only if the generated constraints can be solved.
     */
     pair<expr, constraint_seq> check(expr const & t, level_param_names const & ps = level_param_names());
-    /** \brief Like \c check, but ignores undefined universe level parameters */
-    pair<expr, constraint_seq> check_ignore_levels(expr const & e);
+    /** \brief Like \c check, but ignores undefined universes */
+    pair<expr, constraint_seq> check_ignore_undefined_universes(expr const & e);
 
     /** \brief Return true iff t is definitionally equal to s. */
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s);
diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp
index 1543877e4..3ee31884a 100644
--- a/src/library/tactic/generalize_tactic.cpp
+++ b/src/library/tactic/generalize_tactic.cpp
@@ -39,7 +39,7 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const &
                 expr new_t = mk_pi(n, e_t, abstract(t, *new_e));
                 expr new_m = g.mk_meta(ngen.next(), new_t);
                 try {
-                    tc->check_ignore_levels(g.abstract(new_t));
+                    tc->check_ignore_undefined_universes(g.abstract(new_t));
                 } catch (kernel_exception const & ex) {
                     std::shared_ptr<kernel_exception> ex_ptr(static_cast<kernel_exception*>(ex.clone()));
                     throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {