diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index a8fedf35c2..bb9805c5f7 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_library(library OBJECT expr_lt.cpp io_state.cpp
+add_library(library OBJECT expr_lt.cpp
   bin_app.cpp constants.cpp max_sharing.cpp
   module.cpp sorry.cpp replace_visitor.cpp num.cpp
   class.cpp util.cpp print.cpp annotation.cpp
@@ -6,5 +6,4 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp
   pp_options.cpp projection.cpp
   aux_recursors.cpp trace.cpp
   profiling.cpp time_task.cpp
-  formatter.cpp
-  abstract_type_context.cpp)
+  formatter.cpp)
diff --git a/src/library/abstract_type_context.cpp b/src/library/abstract_type_context.cpp
deleted file mode 100644
index f1ac495258..0000000000
--- a/src/library/abstract_type_context.cpp
+++ /dev/null
@@ -1,15 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/abstract.h"
-#include "library/abstract_type_context.h"
-
-namespace lean {
-push_local_fn::~push_local_fn() {
-    for (unsigned i = 0; i < m_counter; i++)
-        m_ctx.pop_local();
-}
-}
diff --git a/src/library/abstract_type_context.h b/src/library/abstract_type_context.h
deleted file mode 100644
index 7721169128..0000000000
--- a/src/library/abstract_type_context.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*
-Copyright (c) 2016 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"
-
-namespace lean {
-class abstract_type_context {
-    options m_options;
-public:
-    abstract_type_context(options const & opts):m_options(opts) {}
-    abstract_type_context() {}
-    options const & get_options() const { return m_options; }
-    virtual ~abstract_type_context() {}
-    virtual environment const & env() const { lean_unreachable(); }
-    virtual expr whnf(expr const &) { lean_unreachable(); }
-    virtual name next_name() { lean_unreachable(); }
-    virtual expr relaxed_whnf(expr const &) { lean_unreachable(); }
-    virtual bool is_def_eq(expr const &, expr const &) { lean_unreachable(); }
-    virtual bool relaxed_is_def_eq(expr const &, expr const &) { lean_unreachable(); }
-    virtual expr infer(expr const &) { lean_unreachable(); }
-    /** \brief Simular to \c infer, but also performs type checking.
-        \remark Default implementation just invokes \c infer. */
-    virtual expr check(expr const &) { lean_unreachable(); }
-    virtual optional<expr> is_stuck(expr const &) { lean_unreachable(); }
-    virtual optional<name> get_local_pp_name(expr const &) { lean_unreachable(); }
-    virtual expr push_local(name const &, expr const &, binder_info) { lean_unreachable(); }
-    virtual void pop_local() { lean_unreachable(); }
-
-    expr check(expr const &, bool) { lean_unreachable(); }
-};
-
-class push_local_fn {
-    abstract_type_context & m_ctx;
-    unsigned                m_counter;
-public:
-    push_local_fn(abstract_type_context & ctx):m_ctx(ctx), m_counter(0) {}
-    ~push_local_fn();
-    expr operator()(name const & pp_name, expr const & type, binder_info bi = mk_binder_info()) {
-        m_counter++;
-        return m_ctx.push_local(pp_name, type, bi);
-    }
-};
-}
diff --git a/src/library/formatter.cpp b/src/library/formatter.cpp
index e06d0255e1..df85486cd0 100644
--- a/src/library/formatter.cpp
+++ b/src/library/formatter.cpp
@@ -5,19 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <utility>
-#include "util/option_declarations.h"
 #include "library/formatter.h"
 
-#ifndef LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS
-#define LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS false
-#endif
-
 namespace lean {
-static name * g_formatter_hide_full = nullptr;
-
-name const & get_formatter_hide_full_terms_name() { return *g_formatter_hide_full; }
-bool get_formatter_hide_full_terms(options const & opts) { return opts.get_bool(*g_formatter_hide_full, LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS); }
-
 static std::function<void(std::ostream &, expr const & e)> * g_print = nullptr;
 
 void set_print_fn(std::function<void(std::ostream &, expr const &)> const & fn) {
@@ -37,14 +27,9 @@ std::ostream & operator<<(std::ostream & out, expr const & e) {
 void print(lean::expr const & a) { std::cout << a << std::endl; }
 
 void initialize_formatter() {
-    g_formatter_hide_full = new name{"formatter", "hide_full_terms"};
-    mark_persistent(g_formatter_hide_full->raw());
-    register_bool_option(*g_formatter_hide_full, LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS,
-                         "(formatter) replace terms which do not contain metavariables with `...`");
 }
 
 void finalize_formatter() {
-    delete g_formatter_hide_full;
     delete g_print;
 }
 }
diff --git a/src/library/formatter.h b/src/library/formatter.h
index 34d4932015..5fa69883b4 100644
--- a/src/library/formatter.h
+++ b/src/library/formatter.h
@@ -7,31 +7,11 @@ Author: Leonardo de Moura
 #pragma once
 #include <memory>
 #include <utility>
+#include "kernel/expr.h"
 #include "util/options.h"
-#include "util/format.h"
-#include "library/abstract_type_context.h"
 
 namespace lean {
-name const & get_formatter_hide_full_terms_name();
-bool get_formatter_hide_full_terms(options const & opts);
-
-class formatter {
-    std::function<format(expr const &, options const &)> m_fn;
-    options                             m_options;
-public:
-    formatter(options const & o, std::function<format(expr const &, options const &)> const & fn):m_fn(fn), m_options(o) {}
-    format operator()(expr const & e) const { return m_fn(e, m_options); }
-    options const & get_options() const { return m_options; }
-    formatter update_options(options const & o) const { return formatter(o, m_fn); }
-    formatter update_option_if_undef(name const & n, bool v) const { return formatter(m_options.update_if_undef(n, v), m_fn); }
-};
-
-typedef std::function<formatter(environment const &, options const &, abstract_type_context &)> formatter_factory;
-
 std::ostream & operator<<(std::ostream & out, expr const & e);
-
-typedef std::function<format(formatter const &)> pp_fn;
-
 void set_print_fn(std::function<void(std::ostream &, expr const &)> const & fn);
 
 void initialize_formatter();
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 945857099d..6f9a95d3f8 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 #include "library/num.h"
 #include "library/annotation.h"
 #include "library/protected.h"
-#include "library/io_state.h"
 #include "library/print.h"
 #include "library/util.h"
 #include "library/pp_options.h"
@@ -35,7 +34,6 @@ void finalize_library_core_module() {
 
 void initialize_library_module() {
     initialize_print();
-    initialize_io_state();
     initialize_num();
     initialize_annotation();
     initialize_class();
@@ -51,7 +49,6 @@ void finalize_library_module() {
     finalize_class();
     finalize_annotation();
     finalize_num();
-    finalize_io_state();
     finalize_print();
 }
 }
diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp
deleted file mode 100644
index 08ebf4261e..0000000000
--- a/src/library/io_state.cpp
+++ /dev/null
@@ -1,105 +0,0 @@
-/*
-Copyright (c) 2013 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/kernel_exception.h"
-#include "library/print.h"
-#include "library/io_state.h"
-
-namespace lean {
-static io_state * g_dummy_ios = nullptr;
-
-io_state const & get_dummy_ios() {
-    return *g_dummy_ios;
-}
-
-io_state::io_state():io_state(mk_print_formatter_factory()) {}
-
-io_state::io_state(formatter_factory const & fmtf):
-    m_formatter_factory(fmtf),
-    m_regular_channel(std::make_shared<stdout_channel>()),
-    m_diagnostic_channel(std::make_shared<stderr_channel>()) {
-}
-
-io_state::io_state(options const & opts, formatter_factory const & fmtf):
-    m_options(opts),
-    m_formatter_factory(fmtf),
-    m_regular_channel(std::make_shared<stdout_channel>()),
-    m_diagnostic_channel(std::make_shared<stderr_channel>()) {
-}
-io_state::io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> const & d):
-    m_options(ios.m_options),
-    m_formatter_factory(ios.m_formatter_factory),
-    m_regular_channel(r),
-    m_diagnostic_channel(d) {
-}
-io_state::io_state(io_state const & ios, options const & o):
-    m_options(o),
-    m_formatter_factory(ios.m_formatter_factory),
-    m_regular_channel(ios.m_regular_channel),
-    m_diagnostic_channel(ios.m_diagnostic_channel) {
-}
-
-io_state::~io_state() {}
-
-void io_state::set_regular_channel(std::shared_ptr<output_channel> const & out) {
-    if (out)
-        m_regular_channel = out;
-}
-
-void io_state::set_diagnostic_channel(std::shared_ptr<output_channel> const & out) {
-    if (out)
-        m_diagnostic_channel = out;
-}
-
-void io_state::set_options(options const & opts) {
-    m_options = opts;
-}
-
-void io_state::set_formatter_factory(formatter_factory const & f) {
-    m_formatter_factory = f;
-}
-
-LEAN_THREAD_PTR(io_state, g_ios);
-
-io_state const & get_global_ios() {
-    if (g_ios)
-        return *g_ios;
-    else
-        return get_dummy_ios();
-}
-
-scope_global_ios::scope_global_ios(io_state const & ios) {
-    m_old_ios = g_ios;
-    g_ios     = const_cast<io_state*>(&ios);
-}
-
-scope_global_ios::~scope_global_ios() {
-    g_ios = m_old_ios;
-}
-
-char const * formatted_exception::what() const noexcept {
-    if (!m_what_buffer) {
-        options const & opts = get_global_ios().get_options();
-        std::ostringstream out;
-        out << mk_pair(m_fmt, opts);
-        const_cast<formatted_exception*>(this)->m_what_buffer = out.str();
-    }
-    return m_what_buffer->c_str();
-}
-
-options const & get_options_from_ios(io_state const & ios) {
-    return ios.get_options();
-}
-
-void initialize_io_state() {
-    g_dummy_ios = new io_state(mk_print_formatter_factory());
-}
-
-void finalize_io_state() {
-    delete g_dummy_ios;
-}
-}
diff --git a/src/library/io_state.h b/src/library/io_state.h
deleted file mode 100644
index 64edacba06..0000000000
--- a/src/library/io_state.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <string>
-#include "util/output_channel.h"
-#include "util/options.h"
-#include "util/exception_with_pos.h"
-#include "kernel/expr.h"
-#include "library/formatter.h"
-
-namespace lean {
-/**
-   \brief State provided to internal lean procedures that need to:
-   1- Access user defined options
-   2- Produce verbosity messages
-   3- Output results
-   4- Produce formatted output
-*/
-class io_state {
-    options                         m_options;
-    formatter_factory               m_formatter_factory;
-    std::shared_ptr<output_channel> m_regular_channel;
-    std::shared_ptr<output_channel> m_diagnostic_channel;
-public:
-    io_state();
-    io_state(formatter_factory const & fmtf);
-    io_state(options const & opts, formatter_factory const & fmtf);
-    io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> const & d);
-    io_state(io_state const & ios, options const & o);
-    ~io_state();
-
-    options const & get_options() const { return m_options; }
-    formatter_factory const & get_formatter_factory() const { return m_formatter_factory; }
-    std::shared_ptr<output_channel> const & get_regular_channel_ptr() const { return m_regular_channel; }
-    std::shared_ptr<output_channel> const & get_diagnostic_channel_ptr() const { return m_diagnostic_channel; }
-    output_channel & get_regular_channel() const { return *m_regular_channel; }
-    output_channel & get_diagnostic_channel() const { return *m_diagnostic_channel; }
-    std::ostream & get_regular_stream() const { return m_regular_channel->get_stream(); }
-    std::ostream & get_diagnostic_stream() const { return m_diagnostic_channel->get_stream(); }
-
-    void set_regular_channel(std::shared_ptr<output_channel> const & out);
-    void set_diagnostic_channel(std::shared_ptr<output_channel> const & out);
-    void set_options(options const & opts);
-    void set_formatter_factory(formatter_factory const & f);
-    template<typename T> void set_option(name const & n, T const & v) {
-        set_options(get_options().update(n, v));
-    }
-};
-
-/** \brief Return a dummy io_state that is meant to be used in contexts that require an io_state, but it is not really used */
-io_state const & get_dummy_ios();
-
-/** \brief Return reference to thread local io_state object. */
-io_state const & get_global_ios();
-
-/** \brief Formatted exceptions where the format object must be eagerly constructed.
-    This is slightly different from ext_exception where the format object is built on demand. */
-class formatted_exception : public exception_with_pos {
-protected:
-    optional<pos_info>    m_pos;
-    format                m_fmt;
-    optional<std::string> m_what_buffer;
-public:
-    explicit formatted_exception(format const & fmt):m_fmt(fmt) {}
-    formatted_exception(optional<pos_info> const & p, format const & fmt):m_pos(p), m_fmt(fmt) {}
-    virtual char const * what() const noexcept override;
-    virtual optional<pos_info> get_pos() const override { return m_pos; }
-    virtual format pp() const { return m_fmt; }
-};
-
-struct scope_global_ios {
-    io_state * m_old_ios;
-public:
-    scope_global_ios(io_state const & ios);
-    ~scope_global_ios();
-};
-
-options const & get_options_from_ios(io_state const & ios);
-
-void initialize_io_state();
-void finalize_io_state();
-}
diff --git a/src/library/module.h b/src/library/module.h
index 674951de4d..97d12aa416 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -11,7 +11,6 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
 #include <vector>
 #include <lean/serializer.h>
 #include <lean/optional.h>
-#include "library/io_state.h"
 #include "kernel/environment.h"
 
 namespace lean {
diff --git a/src/library/print.cpp b/src/library/print.cpp
index 2d80b1f9c3..5c2276f045 100644
--- a/src/library/print.cpp
+++ b/src/library/print.cpp
@@ -296,17 +296,6 @@ struct print_expr_fn {
     }
 };
 
-formatter_factory mk_print_formatter_factory() {
-    return [](environment const &, options const & o, abstract_type_context &) { // NOLINT
-        return formatter(o, [=](expr const & e, options const &) {
-                std::ostringstream s;
-                print_expr_fn pr(s);
-                pr(e);
-                return format(s.str());
-            });
-    };
-}
-
 void init_default_print_fn() {
     set_print_fn([](std::ostream & out, expr const & e) {
             print_expr_fn pr(out);
diff --git a/src/library/print.h b/src/library/print.h
index 5efbab2c93..98b8892d52 100644
--- a/src/library/print.h
+++ b/src/library/print.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "kernel/expr.h"
 #include "library/formatter.h"
 
 namespace lean {
@@ -21,12 +22,6 @@ name pick_unused_name(expr const & t, name const & s);
 pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type = false);
 pair<expr, expr> let_body_fresh(expr const & b, bool preserve_type = false);
 
-/** \brief Create a simple formatter object based on operator for "print" procedure.
-
-    \remark The print procedure is only used for debugging purposes.
-*/
-formatter_factory mk_print_formatter_factory();
-
 /** \brief Use simple formatter as the default print function */
 void init_default_print_fn();
 
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 7d8afd11d6..ef05a6a4fe 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -65,13 +65,6 @@ optional<expr_pair> is_auto_param(expr const & e) {
     }
 }
 
-level get_level(abstract_type_context & ctx, expr const & A) {
-    expr S = ctx.relaxed_whnf(ctx.infer(A));
-    if (!is_sort(S))
-        throw exception("invalid expression, sort expected");
-    return sort_level(S);
-}
-
 name mk_fresh_lp_name(names const & lp_names) {
     name l("l");
     int i = 1;
@@ -324,20 +317,6 @@ expr instantiate_lparam(expr const & e, name const & p, level const & l) {
     return instantiate_lparams(e, names(p), levels(l));
 }
 
-unsigned get_expect_num_args(abstract_type_context & ctx, expr e) {
-    push_local_fn push_local(ctx);
-    unsigned r = 0;
-    while (true) {
-        e = ctx.whnf(e);
-        if (!is_pi(e))
-            return r;
-        // TODO(Leo): try to avoid the following instantiate.
-        expr local = push_local(binding_name(e), binding_domain(e), binding_info(e));
-        e = instantiate(binding_body(e), local);
-        r++;
-    }
-}
-
 expr to_telescope(bool pi, local_ctx & lctx, name_generator & ngen, expr e, buffer<expr> & telescope, optional<binder_info> const & binfo) {
     while ((pi && is_pi(e)) || (!pi && is_lambda(e))) {
         expr local;
@@ -413,20 +392,6 @@ expr mk_and(expr const & a, expr const & b) {
     return mk_app(*g_and, a, b);
 }
 
-expr mk_and_intro(abstract_type_context & ctx, expr const & Ha, expr const & Hb) {
-    return mk_app(*g_and_intro, ctx.infer(Ha), ctx.infer(Hb), Ha, Hb);
-}
-
-expr mk_and_left(abstract_type_context & ctx, expr const & H) {
-    expr a_and_b = ctx.whnf(ctx.infer(H));
-    return mk_app(*g_and_left, app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
-}
-
-expr mk_and_right(abstract_type_context & ctx, expr const & H) {
-    expr a_and_b = ctx.whnf(ctx.infer(H));
-    return mk_app(*g_and_right, app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
-}
-
 expr mk_unit(level const & l) {
     return mk_constant(get_punit_name(), {l});
 }
@@ -446,34 +411,6 @@ expr mk_unit_mk() {
     return *g_unit_mk;
 }
 
-expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B) {
-    level l1 = get_level(ctx, A);
-    level l2 = get_level(ctx, B);
-    return mk_app(mk_constant(get_pprod_name(), {l1, l2}), A, B);
-}
-
-expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b) {
-    expr A = ctx.infer(a);
-    expr B = ctx.infer(b);
-    level l1 = get_level(ctx, A);
-    level l2 = get_level(ctx, B);
-    return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b);
-}
-
-expr mk_pprod_fst(abstract_type_context & ctx, expr const & p) {
-    expr AxB = ctx.whnf(ctx.infer(p));
-    expr const & A = app_arg(app_fn(AxB));
-    expr const & B = app_arg(AxB);
-    return mk_app(mk_constant(get_pprod_fst_name(), const_levels(get_app_fn(AxB))), A, B, p);
-}
-
-expr mk_pprod_snd(abstract_type_context & ctx, expr const & p) {
-    expr AxB = ctx.whnf(ctx.infer(p));
-    expr const & A = app_arg(app_fn(AxB));
-    expr const & B = app_arg(AxB);
-    return mk_app(mk_constant(get_pprod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p);
-}
-
 static expr * g_nat         = nullptr;
 static expr * g_nat_zero    = nullptr;
 static expr * g_nat_one     = nullptr;
@@ -543,19 +480,6 @@ static void finalize_char() {
 expr mk_unit(level const & l, bool prop) { return prop ? mk_true() : mk_unit(l); }
 expr mk_unit_mk(level const & l, bool prop) { return prop ? mk_true_intro() : mk_unit_mk(l); }
 
-expr mk_pprod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) {
-    return prop ? mk_and(a, b) : mk_pprod(ctx, a, b);
-}
-expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) {
-    return prop ? mk_and_intro(ctx, a, b) : mk_pprod_mk(ctx, a, b);
-}
-expr mk_pprod_fst(abstract_type_context & ctx, expr const & p, bool prop) {
-    return prop ? mk_and_left(ctx, p) : mk_pprod_fst(ctx, p);
-}
-expr mk_pprod_snd(abstract_type_context & ctx, expr const & p, bool prop) {
-    return prop ? mk_and_right(ctx, p) : mk_pprod_snd(ctx, p);
-}
-
 bool is_ite(expr const & e) {
     return is_app_of(e, get_ite_name(), 5);
 }
@@ -593,85 +517,6 @@ expr mk_propext(expr const & lhs, expr const & rhs, expr const & iff_pr) {
     return mk_app(mk_constant(get_propext_name()), lhs, rhs, iff_pr);
 }
 
-expr mk_eq(abstract_type_context & ctx, expr const & lhs, expr const & rhs) {
-    expr A    = ctx.whnf(ctx.infer(lhs));
-    level lvl = get_level(ctx, A);
-    return mk_app(mk_constant(get_eq_name(), {lvl}), A, lhs, rhs);
-}
-
-expr mk_eq_refl(abstract_type_context & ctx, expr const & a) {
-    expr A    = ctx.whnf(ctx.infer(a));
-    level lvl = get_level(ctx, A);
-    return mk_app(mk_constant(get_eq_refl_name(), {lvl}), A, a);
-}
-
-expr mk_eq_symm(abstract_type_context & ctx, expr const & H) {
-    if (is_app_of(H, get_eq_refl_name()))
-        return H;
-    expr p    = ctx.whnf(ctx.infer(H));
-    lean_assert(is_eq(p));
-    expr lhs  = app_arg(app_fn(p));
-    expr rhs  = app_arg(p);
-    expr A    = ctx.infer(lhs);
-    level lvl = get_level(ctx, A);
-    return mk_app(mk_constant(get_eq_symm_name(), {lvl}), A, lhs, rhs, H);
-}
-
-expr mk_eq_trans(abstract_type_context & ctx, expr const & H1, expr const & H2) {
-    if (is_app_of(H1, get_eq_refl_name()))
-        return H2;
-    if (is_app_of(H2, get_eq_refl_name()))
-        return H1;
-    expr p1    = ctx.whnf(ctx.infer(H1));
-    expr p2    = ctx.whnf(ctx.infer(H2));
-    lean_assert(is_eq(p1) && is_eq(p2));
-    expr lhs1  = app_arg(app_fn(p1));
-    expr rhs1  = app_arg(p1);
-    expr rhs2  = app_arg(p2);
-    expr A     = ctx.infer(lhs1);
-    level lvl  = get_level(ctx, A);
-    return mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, lhs1, rhs1, rhs2, H1, H2});
-}
-
-expr mk_eq_subst(abstract_type_context & ctx, expr const & motive,
-                 expr const & x, expr const & y, expr const & xeqy, expr const & h) {
-    expr A    = ctx.infer(x);
-    level l1  = get_level(ctx, A);
-    expr r    = mk_constant(get_eq_subst_name(), {l1});
-    return mk_app({r, A, x, y, motive, xeqy, h});
-}
-
-expr mk_eq_subst(abstract_type_context & ctx, expr const & motive, expr const & xeqy, expr const & h) {
-    expr xeqy_type = ctx.whnf(ctx.infer(xeqy));
-    return mk_eq_subst(ctx, motive, app_arg(app_fn(xeqy_type)), app_arg(xeqy_type), xeqy, h);
-}
-
-expr mk_congr_arg(abstract_type_context & ctx, expr const & f, expr const & H) {
-    expr eq = ctx.relaxed_whnf(ctx.infer(H));
-    expr pi = ctx.relaxed_whnf(ctx.infer(f));
-    expr A, B, lhs, rhs;
-    lean_verify(is_eq(eq, A, lhs, rhs));
-    lean_assert(is_arrow(pi));
-    B = binding_body(pi);
-    level lvl_1  = get_level(ctx, A);
-    level lvl_2  = get_level(ctx, B);
-    return ::lean::mk_app({mk_constant(get_congr_arg_name(), {lvl_1, lvl_2}), A, B, lhs, rhs, f, H});
-}
-
-expr mk_subsingleton_elim(abstract_type_context & ctx, expr const & h, expr const & x, expr const & y) {
-    expr A  = ctx.infer(x);
-    level l = get_level(ctx, A);
-    expr r  = mk_constant(get_subsingleton_elim_name(), {l});
-    return mk_app({r, A, h, x, y});
-}
-
-expr mk_heq(abstract_type_context & ctx, expr const & lhs, expr const & rhs) {
-    expr A    = ctx.whnf(ctx.infer(lhs));
-    expr B    = ctx.whnf(ctx.infer(rhs));
-    level lvl = get_level(ctx, A);
-    return mk_app(mk_constant(get_heq_name(), {lvl}), A, lhs, B, rhs);
-}
-
 bool is_eq_ndrec_core(expr const & e) {
     expr const & fn = get_app_fn(e);
     return is_constant(fn) && const_name(fn) == get_eq_ndrec_name();
@@ -720,14 +565,6 @@ bool is_eq_a_a(expr const & e) {
     return lhs == rhs;
 }
 
-bool is_eq_a_a(abstract_type_context & ctx, expr const & e) {
-    if (!is_eq(e))
-        return false;
-    expr lhs = app_arg(app_fn(e));
-    expr rhs = app_arg(e);
-    return ctx.is_def_eq(lhs, rhs);
-}
-
 bool is_heq(expr const & e) {
     return is_app_of(e, get_heq_name(), 4);
 }
@@ -749,15 +586,6 @@ bool is_heq(expr const & e, expr & lhs, expr & rhs) {
     return is_heq(e, A, lhs, B, rhs);
 }
 
-expr mk_cast(abstract_type_context & ctx, expr const & H, expr const & e) {
-    expr type = ctx.relaxed_whnf(ctx.infer(H));
-    expr A, B;
-    if (!is_eq(type, A, B))
-        throw exception("cast failed, equality proof expected");
-    level lvl = get_level(ctx, A);
-    return mk_app(mk_constant(get_cast_name(), {lvl}), A, B, H, e);
-}
-
 expr mk_false() {
     return mk_constant(get_false_name());
 }
@@ -774,11 +602,6 @@ bool is_empty(expr const & e) {
     return is_constant(e) && const_name(e) == get_empty_name();
 }
 
-expr mk_false_rec(abstract_type_context & ctx, expr const & f, expr const & t) {
-    level t_lvl = get_level(ctx, t);
-    return mk_app(mk_constant(get_false_rec_name(), {t_lvl}), t, f);
-}
-
 bool is_or(expr const & e) {
     return is_app_of(e, get_or_name(), 2);
 }
@@ -823,12 +646,6 @@ expr mk_not(expr const & e) {
     return mk_app(mk_constant(get_not_name()), e);
 }
 
-expr mk_absurd(abstract_type_context & ctx, expr const & t, expr const & e, expr const & not_e) {
-    level t_lvl  = get_level(ctx, t);
-    expr  e_type = ctx.infer(e);
-    return mk_app(mk_constant(get_absurd_name(), {t_lvl}), e_type, t, e, not_e);
-}
-
 bool is_exists(expr const & e, expr & A, expr & p) {
     if (is_app_of(e, get_exists_name(), 2)) {
         A = app_arg(app_fn(e));
diff --git a/src/library/util.h b/src/library/util.h
index 5f8b201d51..59b93ab09c 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/environment.h"
 #include "library/expr_pair.h"
-#include "library/abstract_type_context.h"
 
 namespace lean {
 /* If \c n is not in \c env, then return \c. Otherwise, find the first j >= idx s.t.
@@ -26,11 +25,6 @@ optional<expr> is_optional_param(expr const & e);
 
 optional<expr_pair> is_auto_param(expr const & e);
 
-/** \brief Return the universe level of the type of \c A.
-    Throws an exception if the (relaxed) whnf of the type
-    of A is not a sort. */
-level get_level(abstract_type_context & ctx, expr const & A);
-
 /** brief Return a name that does not appear in `lp_names`. */
 name mk_fresh_lp_name(names const & lp_names);
 
@@ -130,12 +124,6 @@ unsigned get_constructor_idx(environment const & env, name const & n);
     \pre inductive::is_intro_rule(env, ctor_name) */
 name get_constructor_inductive_type(environment const & env, name const & ctor_name);
 
-/** \brief Given an expression \c e, return the number of arguments expected arguments.
-
-    \remark This function counts the number of nested Pi's in \c e. Weak-head-normal-forms are computed for the type of \c e.
-    \remark The type and whnf are computed using \c tc. */
-unsigned get_expect_num_args(abstract_type_context & ctx, expr e);
-
 /** \brief Return the universe where inductive datatype resides
     \pre \c ind_type is of the form <tt>Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}</tt> */
 level get_datatype_level(expr const & ind_type);
@@ -161,28 +149,15 @@ expr mk_true_intro();
 bool is_and(expr const & e, expr & arg1, expr & arg2);
 bool is_and(expr const & e);
 expr mk_and(expr const & a, expr const & b);
-expr mk_and_intro(abstract_type_context & ctx, expr const & Ha, expr const & Hb);
-expr mk_and_elim_left(abstract_type_context & ctx, expr const & H);
-expr mk_and_elim_right(abstract_type_context & ctx, expr const & H);
 
 expr mk_unit(level const & l);
 expr mk_unit_mk(level const & l);
 expr mk_unit();
 expr mk_unit_mk();
 
-expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B);
-expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b);
-expr mk_pprod_fst(abstract_type_context & ctx, expr const & p);
-expr mk_pprod_snd(abstract_type_context & ctx, expr const & p);
-
 expr mk_unit(level const & l, bool prop);
 expr mk_unit_mk(level const & l, bool prop);
 
-expr mk_pprod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
-expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
-expr mk_pprod_fst(abstract_type_context & ctx, expr const & p, bool prop);
-expr mk_pprod_snd(abstract_type_context & ctx, expr const & p, bool prop);
-
 expr mk_nat_type();
 bool is_nat_type(expr const & e);
 expr mk_nat_zero();
@@ -206,19 +181,6 @@ expr mk_iff_refl(expr const & a);
 
 expr mk_propext(expr const & lhs, expr const & rhs, expr const & iff_pr);
 
-expr mk_eq(abstract_type_context & ctx, expr const & lhs, expr const & rhs);
-expr mk_eq_refl(abstract_type_context & ctx, expr const & a);
-expr mk_eq_symm(abstract_type_context & ctx, expr const & H);
-expr mk_eq_trans(abstract_type_context & ctx, expr const & H1, expr const & H2);
-expr mk_eq_subst(abstract_type_context & ctx, expr const & motive,
-                 expr const & x, expr const & y, expr const & xeqy, expr const & h);
-expr mk_eq_subst(abstract_type_context & ctx, expr const & motive, expr const & xeqy, expr const & h);
-
-expr mk_congr_arg(abstract_type_context & ctx, expr const & f, expr const & H);
-
-/** \brief Create an proof for x = y using subsingleton.elim (in standard mode) */
-expr mk_subsingleton_elim(abstract_type_context & ctx, expr const & h, expr const & x, expr const & y);
-
 /** \brief Return true iff \c e is a term of the form (eq.rec ....) */
 bool is_eq_rec_core(expr const & e);
 /** \brief Return true iff \c e is a term of the form (eq.rec ....) */
@@ -231,23 +193,16 @@ bool is_eq(expr const & e, expr & lhs, expr & rhs);
 bool is_eq(expr const & e, expr & A, expr & lhs, expr & rhs);
 /** \brief Return true iff \c e is of the form (eq A a a) */
 bool is_eq_a_a(expr const & e);
-/** \brief Return true iff \c e is of the form (eq A a a') where \c a and \c a' are definitionally equal */
-bool is_eq_a_a(abstract_type_context & ctx, expr const & e);
 
-expr mk_heq(abstract_type_context & ctx, expr const & lhs, expr const & rhs);
 bool is_heq(expr const & e);
 bool is_heq(expr const & e, expr & lhs, expr & rhs);
 bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs);
 
-expr mk_cast(abstract_type_context & ctx, expr const & H, expr const & e);
-
 expr mk_false();
 expr mk_empty();
 
 bool is_false(expr const & e);
 bool is_empty(expr const & e);
-/** \brief Return an element of type t given an element \c f : false */
-expr mk_false_rec(abstract_type_context & ctx, expr const & f, expr const & t);
 
 bool is_or(expr const & e);
 bool is_or(expr const & e, expr & A, expr & B);
@@ -260,9 +215,6 @@ inline bool is_not(expr const & e) { expr a; return is_not(e, a); }
 bool is_not_or_ne(expr const & e, expr & a);
 expr mk_not(expr const & e);
 
-/** \brief Create the term <tt>absurd e not_e : t</tt>. */
-expr mk_absurd(abstract_type_context & ctx, expr const & t, expr const & e, expr const & not_e);
-
 /** \brief Returns none if \c e is not an application with at least two arguments.
     Otherwise it returns <tt>app_fn(app_fn(e))</tt>. */
 optional<expr> get_binary_op(expr const & e);