diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 06900e06d9..96a5c87853 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -131,7 +131,7 @@ struct inductive_cmd_fn {
     }
 
     name mk_rec_name(name const & n) {
-        return n + name("rec");
+        return ::lean::inductive::get_elim_name(n);
     }
 
     /** \brief Parse the name of an inductive datatype or introduction rule,
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index e2ecaff4df..05fb6245c5 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -183,7 +183,7 @@ static environment update(environment const & env, inductive_env_ext const & ext
 }
 
 /**\ brief Return recursor name */
-static name get_elim_name(name const & n) {
+name get_elim_name(name const & n) {
     return n + name("rec");
 }
 
diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h
index 86d0ab3907..39be660fef 100644
--- a/src/kernel/inductive/inductive.h
+++ b/src/kernel/inductive/inductive.h
@@ -72,6 +72,9 @@ bool is_elim_meta_app(type_checker & tc, expr const & e);
     If \c n is not an inductive datatype in \c env, then return none.
 */
 optional<unsigned> get_num_indices(environment const & env, name const & n);
+
+/** \brief Return the eliminator/recursor associated with an inductive datatype */
+name get_elim_name(name const & n);
 }
 void initialize_inductive_module();
 void finalize_inductive_module();