diff --git a/library/init/lean/macro.lean b/library/init/lean/macro.lean
index ae566f2c09..d52bcf72bc 100644
--- a/library/init/lean/macro.lean
+++ b/library/init/lean/macro.lean
@@ -26,7 +26,6 @@ Cases missing:
 -/
 
 inductive macro_definition
-| annotation      : name → macro_definition
 /- The following macros will be Syntax object in Lean4 -/
 | struct_instance : name → bool → list name → macro_definition
 | field_notation  : name → nat → macro_definition
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index d64ae91385..b0173666d5 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -505,7 +505,7 @@ meta def istep {α : Type u} (line0 col0 : ℕ) (line col : ℕ) (t : tactic α)
 
 meta def is_prop (e : expr) : tactic bool :=
 do t ← infer_type e,
-   return (t = `(Prop))
+   return (t = expr.sort level.zero)
 
 /-- Return true iff n is the name of declaration that is a proposition. -/
 meta def is_prop_decl (n : name) : tactic bool :=
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index f4ba235ef5..bd009b3848 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -969,7 +969,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> c
     case expr_kind::FVar:      r = fn; break;
     case expr_kind::Constant:  r = visit_const_core(fn); break;
     case expr_kind::Macro:     r = visit_macro(fn, expected_type, true); break;
-    case expr_kind::MData:     r = visit_mdata(fn, expected_type); break;
+    case expr_kind::MData:     r = visit_mdata(fn, expected_type, true); break;
     case expr_kind::Lambda:    r = visit_lambda(fn, expected_type); break;
     case expr_kind::Let:       r = visit_let(fn, expected_type); break;
     case expr_kind::Quote:
@@ -2525,10 +2525,16 @@ class validate_and_collect_lhs_mvars : public replace_visitor {
         return visit_app(e);
     }
 
-    virtual expr visit_macro(expr const & e) override {
+    virtual expr visit_mdata(expr const & e) override {
         if (is_inaccessible(e)) {
             return e;
-        } else if (is_as_pattern(e)) {
+        } else {
+            return visit(mdata_expr(e));
+        }
+    }
+
+    virtual expr visit_macro(expr const & e) override {
+        if (is_as_pattern(e)) {
             expr new_lhs = visit(get_as_pattern_lhs(e));
             expr new_rhs = visit(get_as_pattern_rhs(e));
             return mk_as_pattern(new_lhs, new_rhs);
@@ -2541,8 +2547,6 @@ class validate_and_collect_lhs_mvars : public replace_visitor {
             return mk_structure_instance(info);
         } else if (auto r = ctx().expand_macro(e)) {
             return visit(*r);
-        } else if (is_synthetic_sorry(e)) {
-            return e;
         } else {
             throw_invalid_pattern("invalid occurrence of macro expression in pattern", e);
             return e;
@@ -2652,7 +2656,7 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
         for (expr const & local_mvar : local_mvars) {
             expr s = instantiate_mvars(local_mvar);
             if (!is_local(s)) {
-                /* The `as_is` macro affects how applications are elaborated.
+                /* The `as_is` annotation affects how applications are elaborated.
                    See comment at first_pass method.
                    So, we only use it if it is really needed. That is,
                    the metavariable was fixed to a non trivial term by type inference rules.
@@ -3355,24 +3359,44 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> const & expecte
     return visit(q, expected_type);
 }
 
-expr elaborator::visit_mdata(expr const & e, optional<expr> const & expected_type) {
-    expr new_e = visit(mdata_expr(e), expected_type);
-    return update_mdata(e, new_e);
-}
-
-expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
+expr elaborator::visit_mdata(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
     if (is_as_is(e)) {
         return get_as_is_arg(e);
+    } else if (is_hole(e)) {
+        return visit_hole(e, expected_type);
+    } else if (is_explicit(e) || is_partial_explicit(e)) {
+        return visit_app_core(e, buffer<expr>(), expected_type, e);
     } else if (is_anonymous_constructor(e)) {
         if (is_app_fn)
             throw elaborator_exception(e, "invalid constructor ⟨...⟩, function expected");
         return visit_anonymous_constructor(e, expected_type);
-    } else if (is_choice(e) || is_explicit(e) || is_partial_explicit(e)) {
-        return visit_app_core(e, buffer<expr>(), expected_type, e);
     } else if (is_by(e)) {
         return visit_by(e, expected_type);
-    } else if (is_hole(e)) {
-        return visit_hole(e, expected_type);
+    } else if (is_as_atomic(e)) {
+        /* ignore annotation */
+        expr new_e = visit(get_as_atomic_arg(e), none_expr());
+        if (is_app_fn)
+            return new_e;
+        /* If the as_atomic macro is not the the function in a function application, then we need to consume
+           implicit arguments. */
+        return visit_base_app_core(new_e, arg_mask::Default, buffer<expr>(), true, expected_type, e);
+    } else if (is_expr_quote(e)) {
+        return visit_expr_quote(e, expected_type);
+    } else if (is_inaccessible(e)) {
+        if (is_app_fn)
+            throw elaborator_exception(e, "invalid inaccessible term, function expected");
+        return visit_inaccessible(e, expected_type);
+    } else if (is_frozen_name(e)) {
+        return visit(get_annotation_arg(e), expected_type);
+    } else {
+        expr new_e = visit(mdata_expr(e), expected_type);
+        return update_mdata(e, new_e);
+    }
+}
+
+expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn) {
+    if (is_choice(e)) {
+        return visit_app_core(e, buffer<expr>(), expected_type, e);
     } else if (is_equations(e)) {
         lean_assert(!is_app_fn); // visit_convoy is used in this case
         return visit_equations(e);
@@ -3388,29 +3412,8 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
         return new_rhs;
     } else if (is_field_notation(e)) {
         return visit_field(e, expected_type);
-    } else if (is_expr_quote(e)) {
-        return visit_expr_quote(e, expected_type);
-    } else if (is_inaccessible(e)) {
-        if (is_app_fn)
-            throw elaborator_exception(e, "invalid inaccessible term, function expected");
-        return visit_inaccessible(e, expected_type);
-    } else if (is_as_atomic(e)) {
-        /* ignore annotation */
-        expr new_e = visit(get_as_atomic_arg(e), none_expr());
-        if (is_app_fn)
-            return new_e;
-        /* If the as_atomic macro is not the the function in a function application, then we need to consume
-           implicit arguments. */
-        return visit_base_app_core(new_e, arg_mask::Default, buffer<expr>(), true, expected_type, e);
-    } else if (is_sorry(e)) {
-        return mk_sorry(expected_type, e, is_synthetic_sorry(e));
     } else if (is_structure_instance(e)) {
         return visit_structure_instance(e, expected_type);
-    } else if (is_frozen_name(e)) {
-        return visit(get_annotation_arg(e), expected_type);
-    } else if (is_annotation(e)) {
-        expr r = visit(get_annotation_arg(e), expected_type);
-        return update_macro(e, 1, &r);
     } else {
         buffer<expr> args;
         for (unsigned i = 0; i < macro_num_args(e); i++)
@@ -3654,7 +3657,7 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
                     }
                     lean_unreachable();
                 case expr_kind::MData:
-                    return copy_pos(e, visit_mdata(e, expected_type));
+                    return copy_pos(e, visit_mdata(e, expected_type, false));
                 case expr_kind::Sort:
                     return copy_pos(e, visit_sort(e));
                 case expr_kind::FVar:
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 7c3bca76c3..130b8981ec 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -236,7 +236,7 @@ private:
     expr visit_macro(expr const & e, optional<expr> const & expected_type, bool is_app_fn);
     expr visit_lambda(expr const & e, optional<expr> const & expected_type);
     expr visit_pi(expr const & e);
-    expr visit_mdata(expr const & e, optional<expr> const & expected_type);
+    expr visit_mdata(expr const & e, optional<expr> const & expected_type, bool is_app_fn);
     expr visit_app(expr const & e, optional<expr> const & expected_type);
     expr visit_let(expr const & e, optional<expr> const & expected_type);
     expr visit_convoy(expr const & e, optional<expr> const & expected_type);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 6ef846c441..72c587117e 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -302,15 +302,12 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
                                        copy_with_new_pos(let_value(e), p),
                                        copy_with_new_pos(let_body(e), p)),
                         p);
-    case expr_kind::Macro:
-        if (is_pexpr_quote(e)) {
-            return save_pos(mk_pexpr_quote(copy_with_new_pos(get_pexpr_quote_value(e), p)), p);
-        } else {
-            buffer<expr> args;
-            for (unsigned i = 0; i < macro_num_args(e); i++)
-                args.push_back(copy_with_new_pos(macro_arg(e, i), p));
-            return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
-        }
+    case expr_kind::Macro: {
+        buffer<expr> args;
+        for (unsigned i = 0; i < macro_num_args(e); i++)
+            args.push_back(copy_with_new_pos(macro_arg(e, i), p));
+        return save_pos(::lean::mk_macro(macro_def(e), args.size(), args.data()), p);
+    }
     case expr_kind::Quote:
         if (is_pexpr_quote(e)) {
             return save_pos(mk_pexpr_quote(copy_with_new_pos(get_pexpr_quote_value(e), p)), p);
@@ -1745,8 +1742,6 @@ static expr quote(expr const & e) {
         return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), mk_expr_placeholder());
     case expr_kind::MVar:
         return mk_expr_placeholder();
-    case expr_kind::MData:
-        throw exception("expr.mdata is not supported at quote function");
     case expr_kind::FVar:
         throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
                                    << mlocal_pp_name(e) << "'");
@@ -1767,13 +1762,14 @@ static expr quote(expr const & e) {
     case expr_kind::Let:
         return mk_app(mk_constant({"expr", "elet"}), mk_expr_placeholder(), quote(let_type(e)),
                       quote(let_value(e)), quote(let_body(e)));
-    case expr_kind::Macro:
+    case expr_kind::MData:
         if (is_antiquote(e))
             return get_antiquote_expr(e);
-        if (is_typed_expr(e))
-            return mk_typed_expr(quote(get_typed_expr_expr(e)), quote(get_typed_expr_type(e)));
-        if (is_inaccessible(e))
+        else if (is_inaccessible(e))
             return mk_expr_placeholder();
+        else
+            throw exception("expr.mdata is not supported at quote function");
+    case expr_kind::Macro:
         throw elaborator_exception(e, sstream() << "invalid quotation, unsupported macro '"
                                    << macro_def(e).get_name() << "'");
     case expr_kind::Quote:
@@ -1874,11 +1870,11 @@ class patexpr_to_expr_fn : public replace_visitor {
         return update_let(e, new_type, new_val, new_body);
     }
 
-    virtual expr visit_macro(expr const & e) override {
+    virtual expr visit_mdata(expr const & e) override {
         if (is_inaccessible(e) && is_placeholder(get_annotation_arg(e))) {
             return get_annotation_arg(e);
         } else {
-            return replace_visitor::visit_macro(e);
+            return replace_visitor::visit_mdata(e);
         }
     }
 
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 78c3668645..7615c8445c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1130,16 +1130,7 @@ auto pretty_fn::pp_macro_default(expr const & e) -> result {
 }
 
 auto pretty_fn::pp_macro(expr const & e) -> result {
-    if (is_explicit(e)) {
-        return pp_explicit(e);
-    } else if (is_expr_quote(e)) {
-        return result(format("`(") + nest(4, pp(get_expr_quote_value(e)).fmt()) + format(")"));
-    } else if (is_pexpr_quote(e)) {
-        return result(format("``(") + nest(2, pp(get_pexpr_quote_value(e)).fmt()) + format(")"));
-    } else if (is_inaccessible(e)) {
-        format r = format(".") + pp_child(get_annotation_arg(e), max_bp()).fmt();
-        return result(r);
-    } else if (is_as_pattern(e)) {
+    if (is_as_pattern(e)) {
         auto lhs_fmt = pp_child(get_as_pattern_lhs(e), max_bp()).fmt();
         auto rhs_fmt = pp_child(get_as_pattern_rhs(e), max_bp()).fmt();
         return result(lhs_fmt + format("@") + rhs_fmt);
@@ -1152,25 +1143,31 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
             return m_unicode ? format("◾") : format("irrel");
         else
             return pp(get_annotation_arg(e));
-    } else if (!m_strings && to_string(e)) {
-        expr n = *macro_def(e).expand(e, m_ctx);
-        return pp(n);
     } else if (is_equations(e)) {
         if (auto r = pp_equations(e))
             return *r;
         else
             return pp_macro_default(e);
+    } else {
+        return pp_macro_default(e);
+    }
+}
+
+auto pretty_fn::pp_mdata(expr const & e) -> result {
+    if (is_explicit(e)) {
+        return pp_explicit(e);
+    } else if (is_expr_quote(e)) {
+        return result(format("`(") + nest(4, pp(get_expr_quote_value(e)).fmt()) + format(")"));
+    } else if (is_inaccessible(e)) {
+        format r = format(".") + pp_child(get_annotation_arg(e), max_bp()).fmt();
+        return result(r);
     } else if (is_annotation(e)) {
         if (m_annotations)
             return format("[") + format(get_annotation_kind(e)) + space() + pp(get_annotation_arg(e)).fmt() + format("]");
         else
             return pp(get_annotation_arg(e));
-    } else if (is_synthetic_sorry(e)) {
-        return m_unicode ? format("⁇") : format("??");
-    } else if (is_sorry(e)) {
-        return format("sorry");
     } else {
-        return pp_macro_default(e);
+        return pp(mdata_expr(e));
     }
 }
 
@@ -1784,7 +1781,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
     case expr_kind::BVar:      return pp_var(e);
     case expr_kind::FVar:      return pp_local(e);
     case expr_kind::Sort:      return pp_sort(e);
-    case expr_kind::MData:     return pp(mdata_expr(e), ignore_hide);
+    case expr_kind::MData:     return pp_mdata(e);
     case expr_kind::Constant:  return pp_const(e);
     case expr_kind::MVar:      return pp_meta(e);
     case expr_kind::App:       return pp_app(e);
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index e31181b369..ddd0a833fd 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -153,6 +153,7 @@ private:
     result pp_explicit(expr const & e);
     result pp_delayed_abstraction(expr const & e);
     result pp_let(expr e);
+    result pp_mdata(expr const & e);
     result pp_num(mpz const & n, unsigned bp);
     result pp_prod(expr const & e);
     result pp_lit(expr const & e);
diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp
index 714afa3997..5ed21733c4 100644
--- a/src/library/annotation.cpp
+++ b/src/library/annotation.cpp
@@ -15,77 +15,26 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name * g_annotation = nullptr;
-static std::string * g_annotation_opcode = nullptr;
 
-name const & get_annotation_name() { return *g_annotation; }
-std::string const & get_annotation_opcode() { return *g_annotation_opcode; }
-
-/** \brief We use a macro to mark expressions that denote "let" and "have"-expressions.
-    These marks have no real semantic meaning, but are useful for helping Lean's pretty printer.
-*/
-class annotation_macro_definition_cell : public macro_definition_cell {
-    name m_name;
-    void check_macro(expr const & m) const {
-        if (!is_macro(m) || macro_num_args(m) != 1)
-            throw exception(sstream() << "invalid '" << m_name << "' annotation, incorrect number of arguments");
-    }
-public:
-    annotation_macro_definition_cell(name const & n):m_name(n) {}
-    name const & get_annotation_kind() const { return m_name; }
-    virtual name get_name() const override { return get_annotation_name(); }
-    virtual void display(std::ostream & out) const override { out << m_name; }
-    virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const override {
-        check_macro(m);
-        return ctx.check(macro_arg(m, 0), infer_only);
-    }
-    virtual optional<expr> expand(expr const & m, abstract_type_context &) const override {
-        check_macro(m);
-        return some_expr(macro_arg(m, 0));
-    }
-    virtual void write(serializer & s) const override {
-        s.write_string(get_annotation_opcode());
-        s << m_name;
-    }
-    virtual bool operator==(macro_definition_cell const & other) const override {
-        if (auto other_ptr = dynamic_cast<annotation_macro_definition_cell const *>(&other)) {
-            return m_name == other_ptr->m_name;
-        } else {
-            return false;
-        }
-    }
-    virtual unsigned hash() const override {
-        return ::lean::hash(m_name.hash(), g_annotation->hash());
-    }
-};
-
-typedef std::unordered_map<name, macro_definition, name_hash, name_eq> annotation_macros;
-static annotation_macros * g_annotation_macros = nullptr;
-
-annotation_macros & get_annotation_macros() { return *g_annotation_macros; }
-
-void register_annotation(name const & n) {
-    annotation_macros & ms = get_annotation_macros();
-    lean_assert(ms.find(n) == ms.end());
-    ms.insert(mk_pair(n, macro_definition(new annotation_macro_definition_cell(n))));
+kvmap mk_annotation_kvmap(name const & k) {
+    return set_name(kvmap(), *g_annotation, k);
 }
 
-expr mk_annotation(name const & kind, expr const & e) {
-    annotation_macros & ms = get_annotation_macros();
-    auto it = ms.find(kind);
-    if (it != ms.end()) {
-        return copy_pos(e, mk_macro(it->second, 1, &e));
-    } else {
-        throw exception(sstream() << "unknown annotation kind '" << kind << "'");
-    }
+typedef std::unordered_map<name, kvmap, name_hash, name_eq> annotation_maps;
+static annotation_maps * g_annotation_maps = nullptr;
+
+void register_annotation(name const & kind) {
+    lean_assert(g_annotation_maps->find(kind) == g_annotation_maps->end());
+    g_annotation_maps->insert(mk_pair(kind, mk_annotation_kvmap(kind)));
 }
 
 bool is_annotation(expr const & e) {
-    return is_macro(e) && macro_def(e).get_name() == get_annotation_name();
+    return is_mdata(e) && get_name(mdata_data(e), *g_annotation);
 }
 
-name const & get_annotation_kind(expr const & e) {
+name get_annotation_kind(expr const & e) {
     lean_assert(is_annotation(e));
-    return static_cast<annotation_macro_definition_cell const*>(macro_def(e).raw())->get_annotation_kind();
+    return *get_name(mdata_data(e), *g_annotation);
 }
 
 bool is_annotation(expr const & e, name const & kind) {
@@ -94,7 +43,19 @@ bool is_annotation(expr const & e, name const & kind) {
 
 expr const & get_annotation_arg(expr const & e) {
     lean_assert(is_annotation(e));
-    return macro_arg(e, 0);
+    return mdata_expr(e);
+}
+
+expr mk_annotation(name const & kind, expr const & e) {
+    auto it = g_annotation_maps->find(kind);
+    if (it != g_annotation_maps->end()) {
+        expr r = copy_pos(e, mk_mdata(it->second, e));
+        lean_assert(is_annotation(r));
+        lean_assert(get_annotation_kind(r) == kind);
+        return r;
+    } else {
+        throw exception(sstream() << "unknown annotation kind '" << kind << "'");
+    }
 }
 
 bool is_nested_annotation(expr const & e, name const & kind) {
@@ -146,26 +107,16 @@ bool is_checkpoint_annotation(expr const & e) { return is_annotation(e, *g_check
 
 void initialize_annotation() {
     g_annotation = new name("annotation");
-    g_annotation_opcode = new std::string("Annot");
-    g_annotation_macros = new annotation_macros();
-    g_have       = new name("have");
-    g_show       = new name("show");
-    g_suffices   = new name("suffices");
-    g_checkpoint = new name("checkpoint");
+    g_annotation_maps = new annotation_maps();
+    g_have            = new name("have");
+    g_show            = new name("show");
+    g_suffices        = new name("suffices");
+    g_checkpoint      = new name("checkpoint");
 
     register_annotation(*g_have);
     register_annotation(*g_show);
     register_annotation(*g_suffices);
     register_annotation(*g_checkpoint);
-
-    register_macro_deserializer(get_annotation_opcode(),
-                                [](deserializer & d, unsigned num, expr const * args) {
-                                    if (num != 1)
-                                        throw corrupted_stream_exception();
-                                    name k;
-                                    d >> k;
-                                    return mk_annotation(k, args[0]);
-                                });
 }
 
 void finalize_annotation() {
@@ -173,8 +124,6 @@ void finalize_annotation() {
     delete g_show;
     delete g_have;
     delete g_suffices;
-    delete g_annotation_macros;
-    delete g_annotation_opcode;
     delete g_annotation;
 }
 }
diff --git a/src/library/annotation.h b/src/library/annotation.h
index ed8530864e..500d0757a5 100644
--- a/src/library/annotation.h
+++ b/src/library/annotation.h
@@ -10,8 +10,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 /** \brief Declare a new kind of annotation. It must only be invoked at startup time
-    Use helper obect #register_annotation_fn.
-*/
+    Use helper obect #register_annotation_fn. */
 void register_annotation(name const & n);
 
 /** \brief Create an annotated expression with tag \c kind based on \c e.
@@ -41,7 +40,7 @@ expr const & get_annotation_arg(expr const & e);
 
     \post get_annotation_arg(mk_annotation(k, e)) == k
 */
-name const & get_annotation_kind(expr const & e);
+name get_annotation_kind(expr const & e);
 
 /** \brief Return the nested annotated expression, \c e must have been created using #mk_annotation.
     This function is the "transitive" version of #get_annotation_arg.
diff --git a/src/library/compiler/eta_expansion.cpp b/src/library/compiler/eta_expansion.cpp
index d395a419af..1ca751ee1b 100644
--- a/src/library/compiler/eta_expansion.cpp
+++ b/src/library/compiler/eta_expansion.cpp
@@ -165,22 +165,6 @@ class eta_expand_fn : public compiler_step_visitor {
         return expand_if_needed(e);
     }
 
-    virtual expr visit_macro(expr const & e) override {
-        if (is_sorry(e)) {
-            /* We η-expand sorrys to be able to execute tactic scripts with syntax errors.
-
-               For example, when we parse and elaborate `by { simp, simmp }`, we get
-               something like `simp >> ??`.
-               With η-expansion, the composite tactic becomes `simp >> (λ s, ?? s)`,
-               and the execution only fails when we arrive at the syntax error.
-            */
-            m_saw_sorry = true;
-            return eta_expand(e);
-        } else {
-            return compiler_step_visitor::visit_macro(e);
-        }
-    }
-
     virtual expr visit_app(expr const & e) override {
         if (is_constant(get_app_fn(e)))
             return expand_if_needed(e);
diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp
index 8580e0b47d..eb79401880 100644
--- a/src/library/compiler/lambda_lifting.cpp
+++ b/src/library/compiler/lambda_lifting.cpp
@@ -205,11 +205,6 @@ class lambda_lifting_fn : public compiler_step_visitor {
         }
     }
 
-    virtual expr visit_macro(expr const & e) override {
-        if (is_sorry(e)) m_saw_sorry = true;
-        return compiler_step_visitor::visit_macro(e);
-    }
-
 public:
     lambda_lifting_fn(environment const & env, abstract_context_cache & cache, name const & prefix):
         compiler_step_visitor(env, cache), m_prefix(prefix), m_idx(1) {
diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index d39a469a14..8e2120e24d 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -274,17 +274,9 @@ class vm_compiler_fn {
         emit(mk_drop_instr(counter));
     }
 
-    void compile_macro(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
-        if (is_annotation(e)) {
-            compile(get_annotation_arg(e), bpz, m);
-        } else if (is_expr_quote(e)) {
-            emit(mk_expr_instr(get_expr_quote_value(e)));
-        } else if (is_pexpr_quote(e)) {
-            emit(mk_expr_instr(get_pexpr_quote_value(e)));
-        } else {
-            throw exception(sstream() << "code generation failed, unexpected kind of macro has been found: '"
-                            << macro_def(e).get_name() << "'");
-        }
+    void compile_macro(expr const & e, unsigned /* bpz */, name_map<unsigned> const & /* m */) {
+        throw exception(sstream() << "code generation failed, unexpected kind of macro has been found: '"
+                        << macro_def(e).get_name() << "'");
     }
 
     void compile_quote(expr const & e) {
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 3a75a48c39..687aa4bdd3 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -223,11 +223,11 @@ bool has_inaccessible_annotation(expr const & e) {
 }
 
 class erase_inaccessible_annotations_fn : public replace_visitor {
-    virtual expr visit_macro(expr const & e) override {
+    virtual expr visit_mdata(expr const & e) override {
         if (is_inaccessible(e)) {
             return visit(get_annotation_arg(e));
         } else {
-            return replace_visitor::visit_macro(e);
+            return replace_visitor::visit_mdata(e);
         }
     }
 };
diff --git a/src/library/metavar_util.h b/src/library/metavar_util.h
index e5057bd6a3..1b708a9dc0 100644
--- a/src/library/metavar_util.h
+++ b/src/library/metavar_util.h
@@ -170,6 +170,10 @@ class instantiate_mvars_fn : public replace_visitor {
             return mk_rev_app(new_f, new_args);
     }
 
+    virtual expr visit_mdata(expr const & e) override {
+        return update_mdata(e, visit(mdata_expr(e)));
+    }
+
     virtual expr visit_macro(expr const & e) override {
         lean_assert(is_macro(e));
         buffer<expr> new_args;
diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index d38b8be3b5..2848826408 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -142,6 +142,14 @@ struct get_noncomputable_reason_fn {
         return !is_sort(type);
     }
 
+    void visit_mdata(expr const & e) {
+        if (is_expr_quote(e) || is_pexpr_quote(e))
+            return;
+        if (should_visit(e)) {
+            visit(mdata_expr(e));
+        }
+    }
+
     void visit_macro(expr const & e) {
         if (is_expr_quote(e) || is_pexpr_quote(e))
             return;
@@ -200,7 +208,7 @@ struct get_noncomputable_reason_fn {
         case expr_kind::Lambda:    visit_binding(e);  return;
         case expr_kind::Pi:        visit_binding(e);  return;
         case expr_kind::Let:       visit_let(e);      return;
-        case expr_kind::MData:     visit(mdata_expr(e)); return;
+        case expr_kind::MData:     visit_mdata(e);    return;
         case expr_kind::Quote:     return;
         }
     }
diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp
index 2b74ff61d8..bd2d490ae2 100644
--- a/src/library/replace_visitor.cpp
+++ b/src/library/replace_visitor.cpp
@@ -24,7 +24,9 @@ expr replace_visitor::visit_mlocal(expr const & e) {
 }
 expr replace_visitor::visit_meta(expr const & e) { return visit_mlocal(e); }
 expr replace_visitor::visit_local(expr const & e) { return visit_mlocal(e); }
-expr replace_visitor::visit_mdata(expr const & e) { return visit(mdata_expr(e)); }
+expr replace_visitor::visit_mdata(expr const & e) {
+    return update_mdata(e, visit(mdata_expr(e)));
+}
 expr replace_visitor::visit_app(expr const & e) {
     lean_assert(is_app(e));
     expr new_fn  = visit(app_fn(e));
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index 7efcc6fa9f..d458d4e830 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -1071,11 +1071,7 @@ simp_result simplify_ext_core_fn::visit_pi(expr const & e) {
 }
 
 simp_result simplify_ext_core_fn::visit_macro(expr const & e) {
-    if (is_annotation(e)) {
-        return visit(get_annotation_arg(e), none_expr());
-    } else {
-        return simplify_core_fn::visit_macro(e);
-    }
+    return simplify_core_fn::visit_macro(e);
 }
 
 simp_result simplify_ext_core_fn::visit_let(expr const & e) {
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index df5dfb3483..2797eb198d 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -737,7 +737,6 @@ optional<expr> type_context_old::reduce_large_elim_recursor(expr const & e) {
     return none_expr();
 }
 
-
 optional<expr> type_context_old::expand_macro(expr const & e) {
     lean_assert(is_macro(e));
     return macro_def(e).expand(e, *this);
@@ -776,9 +775,6 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
     case expr_kind::Constant: case expr_kind::Lit:
         /* Remark: we do not unfold Constants eagerly in this method */
         return e;
-    case expr_kind::MData:
-        e = mdata_expr(e);
-        continue;
     case expr_kind::FVar:
         if (use_zeta() && is_local_decl_ref(e)) {
             if (auto d = m_lctx.find_local_decl(e)) {
@@ -864,7 +860,9 @@ expr type_context_old::whnf_core(expr const & e0, bool proj_reduce) {
             continue;
         }
     }
-
+    case expr_kind::MData:
+        e = mdata_expr(e);
+        continue;
     case expr_kind::Macro:
         if (auto m = expand_macro(e)) {
             check_system("whnf");
@@ -2304,10 +2302,6 @@ struct check_assignment_fn : public replace_visitor {
         }
     }
 
-    expr visit_macro(expr const & e) override {
-        return replace_visitor::visit_macro(e);
-    }
-
     expr operator()(expr const & v) {
         if (!has_expr_metavar(v) && !has_local(v)) {
             return v;
@@ -3343,6 +3337,9 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
             return l_false;
         case expr_kind::Let:
             return l_undef;
+        case expr_kind::MData:
+            it = &mdata_expr(*it);
+            break;
         case expr_kind::Constant:
             if (auto r = constant_is_class(*it)) {
                 result = *r;
@@ -3372,9 +3369,6 @@ lbool type_context_old::is_quick_class(expr const & type, name & result) {
         case expr_kind::Pi:
             it = &binding_body(*it);
             break;
-        case expr_kind::MData:
-            it = &mdata_expr(*it);
-            break;
         case expr_kind::Macro:
             return l_undef;
         case expr_kind::Quote: