diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 9c85cc6d1d..ddce54b81a 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,12 +1,12 @@
 add_library(library OBJECT expr_lt.cpp io_state.cpp
   io_state_stream.cpp bin_app.cpp constants.cpp max_sharing.cpp
-  module.cpp placeholder.cpp sorry.cpp replace_visitor.cpp num.cpp
+  module.cpp sorry.cpp replace_visitor.cpp num.cpp
   class.cpp util.cpp print.cpp annotation.cpp
   protected.cpp reducible.cpp init_module.cpp exception.cpp
   pp_options.cpp projection.cpp
   aux_recursors.cpp trace.cpp
   type_context.cpp
-  locals.cpp messages.cpp message_builder.cpp
+  messages.cpp message_builder.cpp
   profiling.cpp time_task.cpp
   scope_pos_info_provider.cpp formatter.cpp json.cpp
   pos_info_provider.cpp abstract_type_context.cpp)
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 53788852a0..d3e470fddc 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "library/annotation.h"
 #include "library/protected.h"
 #include "library/io_state.h"
-#include "library/placeholder.h"
 #include "library/print.h"
 #include "library/util.h"
 #include "library/pp_options.h"
@@ -40,7 +39,6 @@ void finalize_library_core_module() {
 
 void initialize_library_module() {
     initialize_print();
-    initialize_placeholder();
     initialize_io_state();
     initialize_num();
     initialize_annotation();
@@ -60,7 +58,6 @@ void finalize_library_module() {
     finalize_annotation();
     finalize_num();
     finalize_io_state();
-    finalize_placeholder();
     finalize_print();
 }
 }
diff --git a/src/library/locals.cpp b/src/library/locals.cpp
deleted file mode 100644
index cf195df9f3..0000000000
--- a/src/library/locals.cpp
+++ /dev/null
@@ -1,190 +0,0 @@
-/*
-Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/name_set.h"
-#include "kernel/abstract.h"
-#include "kernel/instantiate.h"
-#include "kernel/expr.h"
-#include "kernel/for_each_fn.h"
-#include "kernel/find_fn.h"
-#include "library/placeholder.h"
-#include "library/locals.h"
-#include "library/pos_info_provider.h"
-
-namespace lean {
-void collect_univ_params_core(level const & l, name_set & r) {
-    for_each(l, [&](level const & l) {
-            if (!has_param(l))
-                return false;
-            if (is_param(l) && !is_placeholder(l))
-                r.insert(param_id(l));
-            return true;
-        });
-}
-
-name_set collect_univ_params(expr const & e, name_set const & ls) {
-    if (!has_param_univ(e)) {
-        return ls;
-    } else {
-        name_set r = ls;
-        for_each(e, [&](expr const & e, unsigned) {
-                if (!has_param_univ(e)) {
-                    return false;
-                } else if (is_sort(e)) {
-                    collect_univ_params_core(sort_level(e), r);
-                } else if (is_constant(e)) {
-                    for (auto const & l : const_levels(e))
-                        collect_univ_params_core(l, r);
-                }
-                return true;
-            });
-        return r;
-    }
-}
-
-names to_names(name_set const & ls) {
-    names r;
-    ls.for_each([&](name const & n) {
-            r = names(n, r);
-        });
-    return r;
-}
-
-void collected_locals::insert(expr const & l) {
-    if (m_local_names.contains(local_name_p(l)))
-        return;
-    m_local_names.insert(local_name_p(l));
-    m_locals.push_back(l);
-}
-
-void collect_locals(expr const & e, collected_locals & ls, bool restricted) {
-    if (!has_local(e))
-        return;
-    expr_set visited;
-    std::function<void(expr const & e)> visit = [&](expr const & e) {
-        if (!has_local(e))
-            return;
-        if (restricted && is_metavar_app(e))
-            return;
-        if (visited.find(e) != visited.end())
-            return;
-        visited.insert(e);
-        switch (e.kind()) {
-        case expr_kind::BVar: case expr_kind::Const:
-        case expr_kind::Sort: case expr_kind::Lit:
-        case expr_kind::MVar:
-            break; // do nothing
-        case expr_kind::MData:
-            visit(mdata_expr(e));
-            break;
-        case expr_kind::Proj:
-            visit(proj_expr(e));
-            break;
-        case expr_kind::FVar:
-            ls.insert(e);
-            break;
-        case expr_kind::App:
-            visit(app_fn(e));
-            visit(app_arg(e));
-            break;
-        case expr_kind::Lambda:
-        case expr_kind::Pi:
-            visit(binding_domain(e));
-            visit(binding_body(e));
-            break;
-        case expr_kind::Let:
-            visit(let_type(e));
-            visit(let_value(e));
-            visit(let_body(e));
-            break;
-        case expr_kind::Local:
-            if (!restricted)
-                visit(local_type(e));
-            ls.insert(e);
-            break;
-        }
-    };
-    visit(e);
-}
-
-/** \brief Return true iff locals(e1) is a subset of locals(e2) */
-bool locals_subset(expr const & e1, expr const & e2) {
-    if (!has_local(e1)) {
-        // empty set is a subset of anything
-        return true;
-    }
-    if (!has_local(e2)) {
-        lean_assert(has_local(e1));
-        return false;
-    }
-    collected_locals S;
-    collect_locals(e2, S);
-    bool is_sub = true;
-    for_each(e1, [&](expr const & e, unsigned) {
-            if (!is_sub || !has_local(e))
-                return false; // stop search
-            if (is_local_or_fvar(e) && !S.contains(e))
-                is_sub = false;
-            return true;
-        });
-    return is_sub;
-}
-
-bool contains_local(expr const & e, name const & n) {
-    if (!has_local(e))
-        return false;
-    bool result = false;
-    for_each(e, [&](expr const & e, unsigned) {
-            if (result || !has_local(e))  {
-                return false;
-            } else if (is_local_or_fvar(e) && local_or_fvar_name(e) == n) {
-                result = true;
-                return false;
-            } else {
-                return true;
-            }
-        });
-    return result;
-}
-
-bool contains_local(expr const & e, name_set const & s) {
-    if (!has_local(e))
-        return false;
-    bool result = false;
-    for_each(e, [&](expr const & e, unsigned) {
-            if (result || !has_local(e))  {
-                return false;
-            } else if (is_local_or_fvar(e) && s.contains(local_or_fvar_name(e))) {
-                result = true;
-                return false;
-            } else {
-                return true;
-            }
-        });
-    return result;
-}
-
-optional<expr> depends_on(unsigned sz, expr const * es, expr const & h) {
-    for (unsigned i = 0; i < sz; i++)
-        if (depends_on(es[i], h))
-            return some_expr(es[i]);
-    return none_expr();
-}
-
-bool depends_on_any(expr const & e, unsigned hs_sz, expr const * hs) {
-    return std::any_of(hs, hs+hs_sz, [&](expr const & h) { return depends_on(e, h); });
-}
-
-expr replace_locals(expr const & e, unsigned sz, expr const * locals, expr const * terms) {
-    return instantiate_rev(abstract_p(e, sz, locals), sz, terms);
-}
-
-expr replace_locals(expr const & e, buffer<expr> const & locals, buffer<expr> const & terms) {
-    lean_assert(locals.size() == terms.size());
-    lean_assert(std::all_of(locals.begin(), locals.end(), is_local_p));
-    return replace_locals(e, locals.size(), locals.data(), terms.data());
-}
-}
diff --git a/src/library/locals.h b/src/library/locals.h
deleted file mode 100644
index ed3fb4fc70..0000000000
--- a/src/library/locals.h
+++ /dev/null
@@ -1,74 +0,0 @@
-/*
-Copyright (c) 2014-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/expr.h"
-#include "kernel/expr_sets.h"
-namespace lean {
-void collect_univ_params_core(level const & l, name_set & r);
-name_set collect_univ_params(expr const & e, name_set const & ls = name_set());
-/**
-  \remark If restricted is true, then locals in meta-variable applications and local constants
-  are ignored.
-*/
-class collected_locals {
-    name_set     m_local_names;
-    buffer<expr> m_locals;
-public:
-    void insert(expr const & l);
-    bool contains(name const & n) const { return m_local_names.contains(n); }
-    bool contains(expr const & l) const { return contains(local_or_fvar_name(l)); }
-    buffer<expr> const & get_collected() const { return m_locals; }
-    bool empty() const { return m_locals.empty(); }
-};
-
-void collect_locals(expr const & e, collected_locals & ls, bool restricted = false);
-
-/** \brief Return true iff locals(e1) is a subset of locals(e2). */
-bool locals_subset(expr const & e1, expr const & e2);
-
-names to_names(name_set const & ls);
-
-/** \brief Return true iff \c [begin_locals, end_locals) contains \c local */
-template<typename It>
-bool contains_local(expr const & local, It const & begin_locals, It const & end_locals) {
-    return std::any_of(begin_locals, end_locals, [&](expr const & l) { return local_or_fvar_name(local) == local_or_fvar_name(l); });
-}
-
-template<typename T>
-bool contains_local(expr const & l, T const & locals) {
-    return std::any_of(locals.begin(), locals.end(),
-                       [&](expr const & l1) { return local_or_fvar_name(l1) == local_or_fvar_name(l); });
-}
-
-/** \brief Return true iff \c e contains a local constant \c h s.t. mlocal_name(h) in s */
-bool contains_local(expr const & e, name_set const & s);
-
-/** \brief Return true iff \c e contains a local constant named \c n (it uses mlocal_name) */
-bool contains_local(expr const & e, name const & n);
-
-/** \brief Return true iff \e contains the local constant \c h */
-inline bool depends_on(expr const & e, expr const & h) {
-    return contains_local(e, local_or_fvar_name(h));
-}
-
-/** \brief Return true iff one of \c es contains the local constant \c h */
-optional<expr> depends_on(unsigned sz, expr const * es, expr const & h);
-
-/** \brief Return true iff \c e depends on any of the local constants in \c hs */
-bool depends_on_any(expr const & e, unsigned hs_sz, expr const * hs);
-inline bool depends_on_any(expr const & e, buffer<expr> const & hs) {
-    return depends_on_any(e, hs.size(), hs.data());
-}
-
-/** \brief Replace the given local constants occurring in \c e with the given terms */
-expr replace_locals(expr const & e, unsigned sz, expr const * locals, expr const * terms);
-expr replace_locals(expr const & e, buffer<expr> const & locals, buffer<expr> const & terms);
-inline expr replace_local(expr const & e, expr const & local, expr const & term) {
-    return replace_locals(e, 1, &local, &term);
-}
-}
diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp
deleted file mode 100644
index 7c9b733db1..0000000000
--- a/src/library/placeholder.cpp
+++ /dev/null
@@ -1,61 +0,0 @@
-/*
-Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <lean/thread.h>
-#include "kernel/find_fn.h"
-#include "library/placeholder.h"
-#include "library/pos_info_provider.h"
-
-namespace lean {
-static name * g_placeholder_name          = nullptr;
-
-void initialize_placeholder() {
-    g_placeholder_name = new name(name::mk_internal_unique_name(), "_");
-    mark_persistent(g_placeholder_name->raw());
-}
-
-void finalize_placeholder() {
-    delete g_placeholder_name;
-}
-
-level mk_level_placeholder() { return mk_univ_mvar(name()); }
-
-expr mk_expr_placeholder() {
-    return mk_mvar(name());
-}
-static bool is_placeholder(name const & n) {
-    return n.is_anonymous();
-}
-bool is_placeholder(level const & e) { return is_mvar(e) && is_placeholder(mvar_id(e)); }
-
-bool is_placeholder(expr const & e) {
-    expr e2 = unwrap_pos(e);
-    return is_mvar(e2) && is_placeholder(mvar_name(e2));
-}
-
-bool has_placeholder(level const & l) {
-    bool r = false;
-    for_each(l, [&](level const & e) {
-            if (is_placeholder(e))
-                r = true;
-            return !r;
-        });
-    return r;
-}
-
-bool has_placeholder(expr const & e) {
-    return (bool) find(e, [](expr const & e, unsigned) { // NOLINT
-            if (is_placeholder(e))
-                return true;
-            else if (is_sort(e))
-                return has_placeholder(sort_level(e));
-            else if (is_constant(e))
-                return std::any_of(const_levels(e).begin(), const_levels(e).end(), [](level const & l) { return has_placeholder(l); });
-            else
-                return false;
-        });
-}
-}
diff --git a/src/library/placeholder.h b/src/library/placeholder.h
deleted file mode 100644
index 726e271124..0000000000
--- a/src/library/placeholder.h
+++ /dev/null
@@ -1,33 +0,0 @@
-/*
-Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-// Placeholders are used to mark locations where additional
-// metavariables should be inserted.
-namespace lean {
-/** \brief Return a new universe level placeholder. */
-level mk_level_placeholder();
-
-/** \brief Return a new expression placeholder expression. */
-expr mk_expr_placeholder();
-
-/** \brief Return true if the given level is a placeholder. */
-bool is_placeholder(level const & e);
-
-/** \brief Return true iff the given expression is a placeholder. */
-bool is_placeholder(expr const & e);
-
-/** \brief Return true iff the given level contains placeholders. */
-bool has_placeholder(level const & l);
-
-/** \brief Return true iff the given expression contains placeholders. */
-bool has_placeholder(expr const & e);
-
-void initialize_placeholder();
-void finalize_placeholder();
-}
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index fccba95bea..bc73682f21 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -23,7 +23,6 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/exception.h"
 #include "library/type_context.h"
-#include "library/locals.h"
 #include "library/aux_recursors.h"
 #include "library/num.h"
 #include "library/time_task.h"
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 94c4cbffff..b4404182ce 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -13,7 +13,6 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/inductive.h"
-#include "library/locals.h"
 #include "library/util.h"
 #include "library/suffixes.h"
 #include "library/annotation.h"
@@ -21,7 +20,6 @@ Author: Leonardo de Moura
 #include "library/pp_options.h"
 #include "library/projection.h"
 #include "library/replace_visitor.h"
-#include "library/type_context.h"
 #include "library/num.h"
 #include "version.h"
 #include "githash.h" // NOLINT