diff --git a/src/library/module.cpp b/src/library/module.cpp
index b2f23d69db..dc8176c132 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -80,7 +80,6 @@ struct module_ext : public environment_extension {
     list<std::shared_ptr<modification const>> m_modifications;
     names        m_module_univs;
     names        m_module_decls;
-    name_set          m_module_defs;
     name_set          m_imported;
     // Map from declaration name to olean file where it was defined
     name_map<std::string>     m_decl2olean;
@@ -391,7 +390,6 @@ environment update_module_defs(environment const & env, declaration const & d) {
     if (d.is_definition()) {
         module_ext ext = get_extension(env);
         ext.m_module_decls = cons(d.get_name(), ext.m_module_decls);
-        ext.m_module_defs.insert(d.get_name());
         return update(env, ext);
     } else {
         module_ext ext = get_extension(env);
@@ -420,11 +418,6 @@ environment add_meta(environment const & env, buffer<declaration> const & ds) {
     return add(new_env, std::make_shared<meta_decls_modification>(to_list(ds)));
 }
 
-bool is_definition(environment const & env, name const & n) {
-    module_ext const & ext = get_extension(env);
-    return ext.m_module_defs.contains(n);
-}
-
 environment add_quot(environment const & env) {
     return add_and_perform(env, std::make_shared<quot_modification>());
 }
diff --git a/src/library/module.h b/src/library/module.h
index 8205957391..8ceac07086 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -139,9 +139,6 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
 environment add(environment const & env, declaration const & d);
 environment add_meta(environment const & env, buffer<declaration> const & ds);
 
-/** \brief Return true iff \c n is a definition added to the current module using #module::add */
-bool is_definition(environment const & env, name const & n);
-
 /** \brief Add the given inductive declaration to the environment, and mark it to be exported. */
 environment add_inductive(environment                       env,
                           inductive::inductive_decl const & decl,