diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 640c2de563..41cfe42de9 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -22,8 +22,6 @@ Author: Leonardo de Moura
 #include "library/pp_options.h"
 #include "library/aux_recursors.h"
 #include "library/private.h"
-#include "library/decl_stats.h"
-#include "library/meng_paulson.h"
 #include "library/fun_info_manager.h"
 #include "library/congr_lemma_manager.h"
 #include "library/abstract_expr_manager.h"
@@ -551,54 +549,6 @@ static environment accessible_cmd(parser & p) {
     return env;
 }
 
-static void display_name_set(parser & p, name const & n, name_set const & s) {
-    if (s.empty())
-        return;
-    io_state_stream out = p.regular_stream();
-    out << "  " << n << " := {";
-    bool first = true;
-    s.for_each([&](name const & n2) {
-            if (is_private(p.env(), n2))
-                return;
-            if (first)
-                first = false;
-            else
-                out << ", ";
-            out << n2;
-        });
-    out << "}\n";
-}
-
-static environment decl_stats_cmd(parser & p) {
-    environment const & env = p.env();
-    io_state_stream out = p.regular_stream();
-    out << "Use sets\n";
-    env.for_each_declaration([&](declaration const & d) {
-            if ((d.is_theorem() || d.is_axiom()) && !is_private(env, d.get_name()))
-                display_name_set(p, d.get_name(), get_use_set(env, d.get_name()));
-        });
-    out << "Used-by sets\n";
-    env.for_each_declaration([&](declaration const & d) {
-            if (!d.is_theorem() && !d.is_axiom() && !is_private(env, d.get_name()))
-                display_name_set(p, d.get_name(), get_used_by_set(env, d.get_name()));
-        });
-    return env;
-}
-
-static environment relevant_thms_cmd(parser & p) {
-    environment const & env = p.env();
-    name_set R;
-    while (p.curr_is_identifier()) {
-        R.insert(p.check_constant_next("invalid #relevant_thms command, constant expected"));
-    }
-    name_set TS = get_relevant_thms(env, p.get_options(), R);
-    io_state_stream out = p.regular_stream();
-    TS.for_each([&](name const & T) {
-            out << T << "\n";
-        });
-    return env;
-}
-
 static void check_expr_and_print(parser & p, expr const & e) {
     environment const & env = p.env();
     type_checker tc(env);
@@ -903,8 +853,6 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#congr_rel",        "(for debugging purposes)", congr_rel_cmd));
     add_cmd(r, cmd_info("#normalizer",       "(for debugging purposes)", normalizer_cmd));
     add_cmd(r, cmd_info("#accessible",       "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
-    add_cmd(r, cmd_info("#decl_stats",       "(for debugging purposes) display declaration statistics", decl_stats_cmd));
-    add_cmd(r, cmd_info("#relevant_thms",    "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd));
     add_cmd(r, cmd_info("#simplify",         "(for debugging purposes) simplify given expression", simplify_cmd));
     add_cmd(r, cmd_info("#abstract_expr",    "(for debugging purposes) call abstract expr methods", abstract_expr_cmd));
 
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index c085c6e107..68c1eaf6ab 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -15,8 +15,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
   relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp
   composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
-  aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp
-  norm_num.cpp class_instance_resolution.cpp type_context.cpp
+  aux_recursors.cpp norm_num.cpp norm_num.cpp class_instance_resolution.cpp type_context.cpp
   tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp
   abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp
   attribute_manager.cpp error_handling.cpp)
diff --git a/src/library/class.cpp b/src/library/class.cpp
index 222c6c8379..3e5ed184e2 100644
--- a/src/library/class.cpp
+++ b/src/library/class.cpp
@@ -15,7 +15,6 @@ Author: Leonardo de Moura
 #include "library/tc_multigraph.h"
 #include "library/protected.h"
 #include "library/class.h"
-#include "library/decl_stats.h"
 #include "library/attribute_manager.h"
 
 namespace lean {
@@ -234,8 +233,7 @@ name get_class_name(environment const & env, expr const & e) {
 
 environment add_class(environment const & env, name const & n, name const & ns, bool persistent) {
     check_class(env, n);
-    environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(n), ns, persistent);
-    return mark_class_instance_somewhere(new_env, n);
+    return class_ext::add_entry(env, get_dummy_ios(), class_entry(n), ns, persistent);
 }
 
 void get_classes(environment const & env, buffer<name> & classes) {
@@ -272,9 +270,8 @@ environment add_instance(environment const & env, name const & n, unsigned prior
     }
     name c = get_class_name(env, get_app_fn(type));
     check_is_class(env, c);
-    environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority),
-                                               ns, persistent);
-    return mark_class_instance_somewhere(new_env, n);
+    return class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority),
+                                ns, persistent);
 }
 
 environment add_instance(environment const & env, name const & n, name const & ns, bool persistent) {
@@ -314,13 +311,11 @@ environment add_trans_instance(environment const & env, name const & n, unsigned
     environment new_env = new_env_insts.first;
     new_env = class_ext::add_entry(new_env, get_dummy_ios(),
                                    class_entry::mk_trans_inst(src_tgt.first, src_tgt.second, n, priority), ns, persistent);
-    new_env = mark_class_instance_somewhere(new_env, n);
     for (tc_edge const & edge : new_env_insts.second) {
         new_env = class_ext::add_entry(new_env, get_dummy_ios(),
                                        class_entry::mk_derived_trans_inst(edge.m_from, edge.m_to, edge.m_cnst), ns, persistent);
         new_env = set_reducible(new_env, edge.m_cnst, reducible_status::Reducible, ns, persistent);
         new_env = add_protected(new_env, edge.m_cnst);
-        new_env = mark_class_instance_somewhere(new_env, edge.m_cnst);
     }
     return new_env;
 }
diff --git a/src/library/decl_stats.cpp b/src/library/decl_stats.cpp
deleted file mode 100644
index 9520fa079f..0000000000
--- a/src/library/decl_stats.cpp
+++ /dev/null
@@ -1,157 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "kernel/environment.h"
-#include "kernel/for_each_fn.h"
-#include "library/reducible.h"
-#include "library/module.h"
-
-namespace lean {
-struct decl_stats_ext : public environment_extension {
-    name_set           m_class_instance; // set of all classes and class instances declared in some namespace
-    name_map<unsigned> m_num_occs;
-    name_map<name_set> m_use_set;
-    name_map<name_set> m_used_by_set;
-
-    void inc_num_occs(name const & n) {
-        if (auto v = m_num_occs.find(n)) {
-            m_num_occs.insert(n, *v+1);
-        } else {
-            m_num_occs.insert(n, 1);
-        }
-    }
-
-    static void updt(name_map<name_set> & s, name const & k, name const & v) {
-        name_set new_set_v;
-        if (auto set_v = s.find(k))
-            new_set_v = *set_v;
-        new_set_v.insert(v);
-        s.insert(k, new_set_v);
-    }
-
-    void updt(name const & user, name const & used) {
-        inc_num_occs(used);
-        updt(m_use_set,     user, used);
-        updt(m_used_by_set, used, user);
-    }
-};
-
-struct decl_stats_ext_reg {
-    unsigned m_ext_id;
-    decl_stats_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<decl_stats_ext>()); }
-};
-
-static decl_stats_ext_reg * g_ext = nullptr;
-static decl_stats_ext const & get_extension(environment const & env) {
-    return static_cast<decl_stats_ext const &>(env.get_extension(g_ext->m_ext_id));
-}
-static environment update(environment const & env, decl_stats_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<decl_stats_ext>(ext));
-}
-
-class update_decl_stats_fn {
-    environment const & m_env;
-    decl_stats_ext      m_ext;
-    name                m_name;
-    name_set            m_visited;
-    name_predicate      m_not_reducible_pred;
-
-    void visit(expr const & e) {
-        for_each(e, [&](expr const & e, unsigned) {
-                if (!is_constant(e))
-                    return true;
-                name const & n = const_name(e);
-                if (m_visited.contains(n))
-                    return true;
-                m_visited.insert(n);
-                if (m_not_reducible_pred(n)) {
-                    m_ext.updt(m_name, n);
-                } else {
-                    // pretend the reducible definition was expanded.
-                    declaration d = m_env.get(n);
-                    visit(d.get_value());
-                }
-                return true;
-            });
-    }
-
-public:
-    update_decl_stats_fn(environment const & env):
-        m_env(env),
-        m_ext(get_extension(env)),
-        m_not_reducible_pred(mk_not_reducible_pred(env)) {}
-
-    environment operator()(declaration const & d) {
-        m_name = d.get_name();
-        visit(d.get_type());
-        return update(m_env, m_ext);
-    }
-};
-
-environment mark_class_instance_somewhere_core(environment const & env, name const & n) {
-    decl_stats_ext ext = get_extension(env);
-    ext.m_class_instance.insert(n);
-    return update(env, ext);
-}
-
-static std::string * g_key = nullptr;
-
-environment mark_class_instance_somewhere(environment const & env, name const & n) {
-    environment new_env = mark_class_instance_somewhere_core(env, n);
-    return module::add(new_env, *g_key, [=](environment const &, serializer & s) { s << n; });
-}
-
-bool is_class_instance_somewhere(environment const & env, name const & n) {
-    return get_extension(env).m_class_instance.contains(n);
-}
-
-static void class_instance_mark_reader(deserializer & d, shared_environment & senv,
-                                       std::function<void(asynch_update_fn const &)> &,
-                                       std::function<void(delayed_update_fn const &)> &) {
-    name n;
-    d >> n;
-    senv.update([=](environment const & env) -> environment {
-            return mark_class_instance_somewhere_core(env, n);
-        });
-}
-
-environment update_decl_stats(environment const & env, declaration const & d) {
-    return update_decl_stats_fn(env)(d);
-}
-
-unsigned get_num_occs(environment const & env, name const & n) {
-    if (auto v = get_extension(env).m_num_occs.find(n))
-        return *v;
-    else
-        return 0;
-}
-
-name_set get_use_set(environment const & env, name const & n) {
-    if (auto v = get_extension(env).m_use_set.find(n))
-        return *v;
-    else
-        return name_set();
-}
-
-name_set get_used_by_set(environment const & env, name const & n) {
-    if (auto v = get_extension(env).m_used_by_set.find(n))
-        return *v;
-    else
-        return name_set();
-}
-
-void initialize_decl_stats() {
-    g_ext = new decl_stats_ext_reg();
-    g_key = new std::string("CIGLB");
-    register_module_object_reader(*g_key, class_instance_mark_reader);
-}
-
-void finalize_decl_stats() {
-    delete g_ext;
-    delete g_key;
-}
-}
diff --git a/src/library/decl_stats.h b/src/library/decl_stats.h
deleted file mode 100644
index 90f7d7f44c..0000000000
--- a/src/library/decl_stats.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-
-namespace lean {
-/** \brief Updated internal indices associated with declarations
-    We track which constants occur in the type of other constants (and the inverse map).
-    We also track the number of times a constant occur in the type of other constants.
-
-    \remark This procedure will "unfold" reducible constants when computing statistics.
-*/
-environment update_decl_stats(environment const & env, declaration const & d);
-/** \brief Return the number of constants s.t. \c n occur in their type. */
-unsigned get_num_occs(environment const & env, name const & n);
-/** \brief Return the set of constants that occur in the type of \c n. */
-name_set get_use_set(environment const & env, name const & n);
-/** \brief Return the set of constants s.t. \c n occur in their type. */
-name_set get_used_by_set(environment const & env, name const & n);
-
-/** \brief Mark that \c n is a class or class-instance in some namespace. */
-environment mark_class_instance_somewhere(environment const & env, name const & n);
-/** \brief Return true iff \c n is a class or class-instance in some namespace. */
-bool is_class_instance_somewhere(environment const & env, name const & n);
-
-void initialize_decl_stats();
-void finalize_decl_stats();
-}
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 55c40c7933..9a31e9f5db 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -42,8 +42,6 @@ Author: Leonardo de Moura
 #include "library/composition_manager.h"
 #include "library/noncomputable.h"
 #include "library/aux_recursors.h"
-#include "library/decl_stats.h"
-#include "library/meng_paulson.h"
 #include "library/class_instance_resolution.h"
 #include "library/type_context.h"
 #include "library/congr_lemma_manager.h"
@@ -90,8 +88,6 @@ void initialize_library_module() {
     initialize_composition_manager();
     initialize_noncomputable();
     initialize_aux_recursors();
-    initialize_decl_stats();
-    initialize_meng_paulson();
     initialize_class_instance_resolution();
     initialize_type_context();
     initialize_light_rule_set();
@@ -105,8 +101,6 @@ void finalize_library_module() {
     finalize_light_rule_set();
     finalize_type_context();
     finalize_class_instance_resolution();
-    finalize_meng_paulson();
-    finalize_decl_stats();
     finalize_aux_recursors();
     finalize_noncomputable();
     finalize_composition_manager();
diff --git a/src/library/meng_paulson.cpp b/src/library/meng_paulson.cpp
deleted file mode 100644
index 6f76908d6b..0000000000
--- a/src/library/meng_paulson.cpp
+++ /dev/null
@@ -1,188 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-
-This module implements a heuristic for selecting relevant theorems based on
-the approach described at
-
-   "Lightweight relevance filtering for machine-generated resolution problems"
-   Jia Meng and Larry Paulson
-   Journal of Applied Logic 7 2009
-*/
-#include <math.h>
-#include "util/sexpr/option_declarations.h"
-#include "kernel/environment.h"
-#include "kernel/inductive/inductive.h"
-#include "library/decl_stats.h"
-#include "library/private.h"
-#include "library/class.h"
-#include "library/constants.h"
-
-#ifndef LEAN_DEFAULT_MENG_PAULSON_P
-#define LEAN_DEFAULT_MENG_PAULSON_P 0.6
-#endif
-
-#ifndef LEAN_DEFAULT_MENG_PAULSON_C
-#define LEAN_DEFAULT_MENG_PAULSON_C 2.4
-#endif
-
-namespace lean {
-static name * g_meng_paulson_p = nullptr;
-static name * g_meng_paulson_c = nullptr;
-
-void initialize_meng_paulson() {
-    g_meng_paulson_p = new name{"meng_paulson", "p"};
-    g_meng_paulson_c = new name{"meng_paulson", "c"};
-
-    register_double_option(*g_meng_paulson_p, LEAN_DEFAULT_MENG_PAULSON_P,
-                           "(theorem selection) control parameter for the Meng&Paulson theorem selection heuristic"
-                           "(for details see paper \"Lightweight relevance filtering for machine-generated resolution problems)\"");
-    register_double_option(*g_meng_paulson_c, LEAN_DEFAULT_MENG_PAULSON_C,
-                           "(theorem selection) control parameter for the Meng&Paulson theorem selection heuristic"
-                           "(for details see paper \"Lightweight relevance filtering for machine-generated resolution problems)\"");
-}
-
-void finalize_meng_paulson() {
-    delete g_meng_paulson_p;
-    delete g_meng_paulson_c;
-}
-
-double get_meng_paulson_p(options const & o) {
-    return o.get_double(*g_meng_paulson_p, LEAN_DEFAULT_MENG_PAULSON_P);
-}
-
-double get_meng_paulson_c(options const & o) {
-    return o.get_double(*g_meng_paulson_c, LEAN_DEFAULT_MENG_PAULSON_C);
-}
-
-class relevant_thms_fn {
-    environment m_env;
-    double      m_p;
-    double      m_c;
-    name_set    m_relevant;
-
-    double get_weight(name const & n) const {
-        double r = get_num_occs(m_env, n);
-        return 1.0 + 2.0 / log(r + 1.0);
-    }
-
-    bool is_connective(name const & n) const {
-        return
-            n == get_or_name() ||
-            n == get_and_name() ||
-            n == get_not_name() ||
-            n == get_iff_name() ||
-            n == get_not_name() ||
-            n == get_ite_name() ||
-            n == get_true_name() ||
-            n == get_false_name();
-    }
-
-    // constants symbols in theorem types that should be ignored
-    bool ignore_F(name const & F) const {
-        if (is_private(m_env, F))
-            return true; // we ignore private decls
-        if (is_class_instance_somewhere(m_env, F))
-            return true; // ignore if F is a class or class-instance in some namespace
-        if (is_connective(F))
-            return true;
-        return false;
-    }
-
-    // Theorems/Axioms that should be ignored
-    bool ignore_T(name const & T) const {
-        if (is_private(m_env, T))
-            return true;
-        if (inductive::is_elim_rule(m_env, T))
-            return true;
-        if (inductive::is_intro_rule(m_env, T))
-            return true;
-        return false;
-    }
-
-    double get_thm_score(name const & n) const {
-        name_set s  = get_use_set(m_env, n);
-        unsigned IR = 0;
-        double M = 0.0;
-        s.for_each([&](name const & F) {
-                if (ignore_F(F))
-                    return;
-                if (m_relevant.contains(F)) {
-                    M += get_weight(F);
-                } else {
-                    // std::cout << "IR: " << F << "\n";
-                    IR++;
-                }
-            });
-        // std::cout << n << " M: " << M << " IR: " << IR << "\n";
-        if (M > 0.0)
-            return M / (M + IR);
-        else
-            return 0.0;
-    }
-public:
-    relevant_thms_fn(environment const & env, double p, double c, name_set const & rel):
-        m_env(env), m_p(p), m_c(c), m_relevant(rel) {
-        lean_assert(c > 0.0);
-    }
-
-    name_set operator()() {
-        name_set A;
-        name_set Fs = m_relevant;
-        // unsigned i = 1;
-        while (true) {
-            // std::cout << "#" << i << ", p: " << m_p << "\n";
-            name_set Rel;
-            Fs.for_each([&](name const & F) {
-                    name_set used_by = get_used_by_set(m_env, F);
-                    used_by.for_each([&](name const & T) {
-                            declaration const & T_decl = m_env.get(T);
-                            if (A.contains(T))
-                                return; // T is already in the result set
-                            if (!T_decl.is_theorem() && !T_decl.is_axiom())
-                                return; // we only care about axioms and theorems
-                            if (ignore_T(T))
-                                return; // we ignore private decls
-                            double M = get_thm_score(T);
-                            // std::cout << T << " : " << M << "\n";
-                            if (M < m_p)
-                                return; // score is to low
-                            Rel.insert(T);
-                            A.insert(T);
-                        });
-                });
-            if (Rel.empty())
-                break;
-            // include symbols of new theorems in m_relevant
-            Fs = name_set(); // reset Fs
-            Rel.for_each([&](name const & T) {
-                    name_set uses = get_use_set(m_env, T);
-                    uses.for_each([&](name const & F) {
-                            declaration const & F_decl = m_env.get(F);
-                            if (F_decl.is_theorem() || F_decl.is_axiom())
-                                return; // we ignore theorems occurring in types
-                            if (ignore_F(F))
-                                return;
-                            // if (!m_relevant.contains(F))
-                            //    std::cout << "new relevant: " << F << "\n";
-                            m_relevant.insert(F);
-                            Fs.insert(F);
-                        });
-                });
-            m_p = m_p + (1.0 - m_p) / m_c;
-        }
-        return A;
-    }
-};
-
-name_set get_relevant_thms(environment const & env, double p, double c,
-                           name_set const & relevant_symbols) {
-    return relevant_thms_fn(env, p, c, relevant_symbols)();
-}
-
-name_set get_relevant_thms(environment const & env, options const & o, name_set const & relevant_symbols) {
-    return relevant_thms_fn(env, get_meng_paulson_p(o), get_meng_paulson_c(o), relevant_symbols)();
-}
-}
diff --git a/src/library/meng_paulson.h b/src/library/meng_paulson.h
deleted file mode 100644
index adc19e33a9..0000000000
--- a/src/library/meng_paulson.h
+++ /dev/null
@@ -1,16 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/name_set.h"
-#include "kernel/environment.h"
-
-namespace lean {
-name_set get_relevant_thms(environment const & env, double p, double c, name_set const & relevant_symbols);
-name_set get_relevant_thms(environment const & env, options const & o, name_set const & relevant_symbols);
-void initialize_meng_paulson();
-void finalize_meng_paulson();
-}
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 250949ea59..3ef15c2f56 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -29,7 +29,6 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/kernel_serializer.h"
 #include "library/unfold_macros.h"
-#include "library/decl_stats.h"
 #include "version.h"
 
 #ifndef LEAN_ASYNCH_IMPORT_THEOREM
@@ -223,7 +222,6 @@ static environment export_decl(environment const & env, declaration const & d) {
 environment add(environment const & env, certified_declaration const & d) {
     environment new_env = env.add(d);
     declaration _d = d.get_declaration();
-    new_env = update_decl_stats(new_env, _d);
     if (!check_computable(new_env, _d.get_name()))
         new_env = mark_noncomputable(new_env, _d.get_name());
     return export_decl(update_module_defs(new_env, _d), _d);
diff --git a/src/library/shared_environment.cpp b/src/library/shared_environment.cpp
index a925c7ed51..96e90ef470 100644
--- a/src/library/shared_environment.cpp
+++ b/src/library/shared_environment.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/shared_environment.h"
-#include "library/decl_stats.h"
 
 namespace lean {
 shared_environment::shared_environment() {}
@@ -19,13 +18,11 @@ environment shared_environment::get_environment() const {
 void shared_environment::add(certified_declaration const & d) {
     lock_guard<mutex> l(m_mutex);
     m_env = m_env.add(d);
-    m_env = update_decl_stats(m_env, d.get_declaration());
 }
 
 void shared_environment::add(declaration const & d) {
     lock_guard<mutex> l(m_mutex);
     m_env = m_env.add(d);
-    m_env = update_decl_stats(m_env, d);
 }
 
 void shared_environment::replace(certified_declaration const & t) {