diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp
index dda40848b..7b2d3a494 100644
--- a/src/library/definitional/projection.cpp
+++ b/src/library/definitional/projection.cpp
@@ -90,78 +90,6 @@ bool is_structure(environment const & env, name const & S) {
     return length(inductive::inductive_decl_intros(decl)) == 1 && *inductive::get_num_indices(env, S) == 0;
 }
 
-/** \brief If \c is a constructor application, then return the name of the constructor.
-    Otherwise, return none.
-*/
-optional<name> is_constructor_app(environment const & env, expr const & e) {
-    expr const & fn = get_app_fn(e);
-    if (is_constant(fn))
-        if (auto I = inductive::is_intro_rule(env, const_name(fn)))
-            return optional<name>(const_name(fn));
-    return optional<name>();
-}
-
-/** \brief If \c d is the name of a definition of the form
-            Fun (a : A), t
-    where t is a constructor application, then return the name of the constructor.
-*/
-optional<name> is_constructor_app_def(environment const & env, name const & d) {
-    if (auto decl = env.find(d)) {
-        expr const * it = &decl->get_value();
-        while (is_lambda(*it))
-            it = &binding_body(*it);
-        return is_constructor_app(env, *it);
-    }
-    return optional<name>();
-}
-
-/** \brief Return the name of constructor and projection functions iff \c e is of the form
-
-        (mk ... (pr ...) ...)
-
-    where \c mk is a constructor of a structure, and at least of the arguments is a projection \c pr
-    where \c pr is not necessarily a projection associated with \c mk.
-    In this case, the name of \c pr is returned. Otherwise, none is returned.
-*/
-optional<pair<name, name>> is_constructor_of_projections(environment const & env, expr const & e) {
-    expr const & fn = get_app_fn(e);
-    if (is_constant(fn)) {
-        if (auto I = inductive::is_intro_rule(env, const_name(fn))) {
-            if (is_structure(env, *I)) {
-                expr const * it = &e;
-                while (is_app(*it)) {
-                    expr const & arg = app_arg(*it);
-                    expr const & pr  = get_app_fn(arg);
-                    if (is_constant(pr)) {
-                        if (auto info = get_projection_info(env, const_name(pr))) {
-                            if (info->m_nparams + 1 == get_app_num_args(arg))
-                                return some(mk_pair(const_name(pr), const_name(pr)));
-                        }
-                    }
-                    it = &app_fn(*it);
-                }
-            }
-        }
-    }
-    return optional<pair<name, name>>();
-}
-
-/** \brief Return the name of constructor and projection functions iff \c d is the name of a definition of the form
-
-       Fun (a : A), t
-
-    where is_constructor_of_projections(env, t)
- */
-optional<pair<name, name>> is_constructor_of_projections_def(environment const & env, name const & d) {
-    if (auto decl = env.find(d)) {
-        expr const * it = &decl->get_value();
-        while (is_lambda(*it))
-            it = &binding_body(*it);
-        return is_constructor_of_projections(env, *it);
-    }
-    return optional<pair<name, name>>();
-}
-
 [[ noreturn ]] static void throw_ill_formed(name const & n) {
     throw exception(sstream() << "projection generation, '" << n << "' is an ill-formed inductive datatype");
 }