diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index a7442c3c43..51d408a000 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -4,7 +4,7 @@ parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
 notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmds.cpp dependencies.cpp
 pp.cpp structure_cmd.cpp structure_instance.cpp
-init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp
+init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp
 opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp elaborator_exception.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
 brackets.cpp tactic_notation.cpp)
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 06734f7021..a124719d67 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -29,7 +29,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
-#include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/match_expr.h"
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/brackets.h"
@@ -722,7 +721,6 @@ parse_table init_nud_table() {
     r = r.add({transition("suppose", mk_ext_action(parse_suppose))}, x0);
     r = r.add({transition("show", mk_ext_action(parse_show))}, x0);
     r = r.add({transition("suffices", mk_ext_action(parse_suffices))}, x0);
-    r = r.add({transition("abstract", mk_ext_action(parse_nested_declaration))}, x0);
     r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);
     r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
     r = r.add({transition("(", Expr), transition(":", Expr), transition(")", mk_ext_action(parse_typed_expr))}, x0);
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 4de08df6ad..127c7c259c 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -28,7 +28,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/update_environment_exception.h"
-#include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/definition_cmds.h"
 #include "frontends/lean/inductive_cmds.h"
diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp
index fad1e8a73c..38a01abe8e 100644
--- a/src/frontends/lean/init_module.cpp
+++ b/src/frontends/lean/init_module.cpp
@@ -18,7 +18,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/pp.h"
 #include "frontends/lean/local_ref_info.h"
 #include "frontends/lean/decl_cmds.h"
-#include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/prenum.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/match_expr.h"
@@ -44,7 +43,6 @@ void initialize_frontend_lean_module() {
     initialize_pp();
     initialize_local_ref_info();
     initialize_decl_cmds();
-    initialize_nested_declaration();
     initialize_match_expr();
     initialize_elaborator();
     initialize_notation_cmd();
@@ -55,7 +53,6 @@ void finalize_frontend_lean_module() {
     finalize_notation_cmd();
     finalize_elaborator();
     finalize_match_expr();
-    finalize_nested_declaration();
     finalize_decl_cmds();
     finalize_local_ref_info();
     finalize_pp();
diff --git a/src/frontends/lean/nested_declaration.cpp b/src/frontends/lean/nested_declaration.cpp
deleted file mode 100644
index e1862a2e96..0000000000
--- a/src/frontends/lean/nested_declaration.cpp
+++ /dev/null
@@ -1,214 +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 "util/sstream.h"
-#include "util/fresh_name.h"
-#include "kernel/type_checker.h"
-#include "kernel/find_fn.h"
-#include "kernel/instantiate.h"
-#include "kernel/abstract.h"
-#include "library/locals.h"
-#include "library/scoped_ext.h"
-#include "library/kernel_serializer.h"
-#include "library/replace_visitor.h"
-#include "library/module.h"
-#include "library/aliases.h"
-#include "frontends/lean/tokens.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/util.h"
-#include "frontends/lean/nested_declaration.h"
-
-namespace lean {
-static name * g_nested_decl = nullptr;
-static std::string * g_nested_decl_opcode = nullptr;
-
-name const & get_nested_decl_name() { return *g_nested_decl; }
-std::string const & get_nested_decl_opcode() { return *g_nested_decl_opcode; }
-
-class nested_decl_macro_definition_cell : public macro_definition_cell {
-    optional<name>  m_name;
-
-    void check_macro(expr const & m) const {
-        if (!is_macro(m) || macro_num_args(m) != 1)
-            throw exception(sstream() << "invalid nested declaration, incorrect number of arguments");
-    }
-public:
-    nested_decl_macro_definition_cell(optional<name> const & n):
-        m_name(n) {}
-    virtual name get_name() const { return get_nested_decl_name(); }
-    virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const {
-        check_macro(m);
-        return ctx.check(macro_arg(m, 0), infer_only);
-    }
-    virtual optional<expr> expand(expr const & m, abstract_type_context &) const {
-        check_macro(m);
-        return some_expr(macro_arg(m, 0));
-    }
-    virtual void write(serializer & s) const {
-        s.write_string(get_nested_decl_opcode());
-        s << m_name;
-    }
-    virtual unsigned hash() const {
-        return get_nested_decl_name().hash();
-    }
-    optional<name> const & get_decl_name() const { return m_name; }
-};
-
-expr mk_nested_declaration(optional<name> const & n, expr const & e) {
-    macro_definition def(new nested_decl_macro_definition_cell(n));
-    return mk_macro(def, 1, &e);
-}
-
-bool is_nested_declaration(expr const & e) {
-    return is_macro(e) && macro_def(e).get_name() == get_nested_decl_name();
-}
-
-expr update_nested_declaration(expr const & e, expr const & new_d) {
-    lean_assert(is_nested_declaration(e));
-    return mk_macro(macro_def(e), 1,  &new_d);
-}
-
-expr get_nested_declaration_arg(expr const & e) {
-    lean_assert(is_nested_declaration(e));
-    return macro_arg(e, 0);
-}
-
-optional<name> const & get_nested_declaration_name(expr const & d) {
-    lean_assert(is_nested_declaration(d));
-    return static_cast<nested_decl_macro_definition_cell const*>(macro_def(d).raw())->get_decl_name();
-}
-
-LEAN_THREAD_VALUE(bool, g_allow_nested_declarations, false);
-
-allow_nested_decls_scope::allow_nested_decls_scope(bool enable) {
-    m_saved = g_allow_nested_declarations;
-    g_allow_nested_declarations = enable;
-}
-
-allow_nested_decls_scope::~allow_nested_decls_scope() {
-    g_allow_nested_declarations = m_saved;
-}
-
-expr parse_nested_declaration(parser & p, unsigned, expr const *, pos_info const & pos) {
-    try {
-        optional<name> n;
-        if (!g_allow_nested_declarations)
-            throw parser_error("invalid 'abstract' expression, it is only allowed inside definitions", pos);
-        if (p.curr_is_token(get_as_tk())) {
-            p.next();
-            n = p.check_id_next("invalid 'abstract' expression, identifier expected");
-        }
-        expr e = p.parse_expr();
-        p.check_token_next(get_end_tk(), "invalid 'abstract' expression, 'end' expected");
-        return p.save_pos(mk_nested_declaration(n, e), pos);
-    } catch (exception & ex) {
-        consume_until_end(p);
-        ex.rethrow();
-        lean_unreachable();
-    }
-}
-
-bool contains_nested_declarations(expr const & e) {
-    return static_cast<bool>(find(e, [&](expr const & n, unsigned) { return is_nested_declaration(n); }));
-}
-
-class extractor : public replace_visitor {
-    environment  m_env;
-    io_state     m_ios;
-    type_checker m_tc;
-    name         m_dname;
-    unsigned     m_idx;
-public:
-    extractor(environment const & env, io_state const & ios, name const & dname):
-        m_env(env), m_ios(ios), m_tc(m_env), m_dname(dname), m_idx(1) {}
-
-    name mk_name_for(expr const & e) {
-        lean_assert(is_nested_declaration(e));
-        if (auto n = get_nested_declaration_name(e)) {
-            return *n;
-        } else {
-            name ns  = get_namespace(m_env);
-            while (true) {
-                name aux = m_dname.append_after(m_idx);
-                m_idx++;
-                if (!m_env.find(ns + aux))
-                    return aux;
-            }
-        }
-    }
-
-    expr extract(expr const & e) {
-        lean_assert(is_nested_declaration(e));
-        expr const & d = visit(get_nested_declaration_arg(e));
-        name new_name      = mk_name_for(e);
-        name new_real_name = get_namespace(m_env) + new_name;
-        collected_locals locals;
-        collect_locals(d, locals);
-        buffer<name> uparams;
-        collect_univ_params(d).to_buffer(uparams);
-        expr new_value           = Fun(locals.get_collected(), d);
-        expr new_type            = m_tc.infer(new_value);
-        level_param_names new_ps = to_list(uparams);
-        levels ls                = param_names_to_levels(new_ps);
-        m_env = module::add(m_env, check(m_env, mk_definition(m_env, new_real_name, new_ps,
-                                                              new_type, new_value)));
-        if (new_name != new_real_name)
-            m_env = add_expr_alias_rec(m_env, new_name, new_real_name);
-        return mk_app(mk_constant(new_real_name, ls), locals.get_collected());
-    }
-
-    expr visit_macro(expr const & e) override {
-        if (is_nested_declaration(e)) {
-            return extract(e);
-        } else {
-            return replace_visitor::visit_macro(e);
-        }
-    }
-
-    expr visit_binding(expr const & b) override {
-        expr new_domain = visit(binding_domain(b));
-        expr l          = mk_local(mk_fresh_name(), new_domain);
-        expr new_body   = abstract(visit(instantiate(binding_body(b), l)), l);
-        return update_binding(b, new_domain, new_body);
-    }
-
-    expr visit_let(expr const & e) override {
-        // TODO(Leo): improve
-        return visit(instantiate(let_body(e), let_value(e)));
-    }
-
-    environment const & get_env() const { return m_env; }
-};
-
-std::tuple<environment, expr> extract_nested_declarations(environment const & env, io_state const & ios,
-                                                          name const & dname, expr const & e) {
-    if (contains_nested_declarations(e)) {
-        extractor ex(env, ios, dname);
-        expr new_e = ex(e);
-        return std::make_tuple(ex.get_env(), new_e);
-    } else {
-        return std::make_tuple(env, e);
-    }
-}
-
-void initialize_nested_declaration() {
-    g_nested_decl        = new name("nested_decl");
-    g_nested_decl_opcode = new std::string("NDecl");
-    register_macro_deserializer(get_nested_decl_opcode(),
-                                [](deserializer & d, unsigned num, expr const * args) {
-                                    if (num != 1)
-                                        throw corrupted_stream_exception();
-                                    optional<name> n;
-                                    d >> n;
-                                    return mk_nested_declaration(n, args[0]);
-                                });
-}
-void finalize_nested_declaration() {
-    delete g_nested_decl;
-    delete g_nested_decl_opcode;
-}
-}
diff --git a/src/frontends/lean/nested_declaration.h b/src/frontends/lean/nested_declaration.h
deleted file mode 100644
index 4ade145d23..0000000000
--- a/src/frontends/lean/nested_declaration.h
+++ /dev/null
@@ -1,24 +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/flet.h"
-#include "kernel/expr.h"
-namespace lean {
-class parser;
-// auxiliary object used to temporarily enable nested declarations
-class allow_nested_decls_scope {
-    bool m_saved;
-public:
-    allow_nested_decls_scope(bool enable = true);
-    ~allow_nested_decls_scope();
-};
-expr parse_nested_declaration(parser & p, unsigned, expr const *, pos_info const & pos);
-std::tuple<environment, expr> extract_nested_declarations(environment const & env, io_state const & ios,
-                                                          name const & def_name, expr const & e);
-void initialize_nested_declaration();
-void finalize_nested_declaration();
-}
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 6c678b2d04..70d95be3b0 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -21,7 +21,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/decl_attributes.h"
 
 namespace lean {
@@ -724,7 +723,6 @@ static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, notation
 }
 
 static environment notation_cmd(parser & p) {
-    allow_nested_decls_scope scope(true);
     bool overload = true;
     notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
@@ -732,7 +730,6 @@ static environment notation_cmd(parser & p) {
 }
 
 static environment infixl_cmd(parser & p) {
-    allow_nested_decls_scope scope(true);
     bool overload = true;
     notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
@@ -740,7 +737,6 @@ static environment infixl_cmd(parser & p) {
 }
 
 static environment infixr_cmd(parser & p) {
-    allow_nested_decls_scope scope(true);
     bool overload = true;
     notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
@@ -748,7 +744,6 @@ static environment infixr_cmd(parser & p) {
 }
 
 static environment postfix_cmd(parser & p) {
-    allow_nested_decls_scope scope(true);
     bool overload = true;
     notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
@@ -756,7 +751,6 @@ static environment postfix_cmd(parser & p) {
 }
 
 static environment prefix_cmd(parser & p) {
-    allow_nested_decls_scope scope(true);
     bool overload = true;
     notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
@@ -790,7 +784,6 @@ static environment dispatch_notation_cmd(parser & p, bool overload, notation_ent
 }
 
 environment local_notation_cmd(parser & p) {
-    allow_nested_decls_scope scope(true);
     parser::in_notation_ctx ctx(p);
     bool overload   = false; // REMARK: local notation override global one
     notation_entry_group grp = notation_entry_group::Main;