diff --git a/src/library/local_context.h b/src/library/local_context.h
index 80e84f250a..c921e177ac 100644
--- a/src/library/local_context.h
+++ b/src/library/local_context.h
@@ -35,7 +35,6 @@ private:
     friend class local_context;
     friend void initialize_local_context();
     local_decl(unsigned idx, name const & n, name const & pp_n, expr const & t, optional<expr> const & v, binder_info const & bi);
-    unsigned get_idx() const { return m_ptr->m_idx; }
 public:
     local_decl();
     local_decl(local_decl const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
@@ -52,6 +51,7 @@ public:
     optional<expr> const & get_value() const { return m_ptr->m_value; }
     binder_info const & get_info() const { return m_ptr->m_bi; }
     expr mk_ref() const;
+    unsigned get_idx() const { return m_ptr->m_idx; }
 };
 
 bool is_local_decl_ref(expr const & e);
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 06fed1a4c2..c1939a65a4 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -190,7 +190,8 @@ expr type_context::revert_core(unsigned num, expr const * locals, expr const & m
 
 expr type_context::revert(unsigned num, expr const * locals, expr const & mvar) {
     lean_assert(is_metavar_decl_ref(mvar));
-    lean_assert(std::all_of(locals, locals+num, [&](expr const & l) { return mvar.get_context().contains(l); }));
+    lean_assert(std::all_of(locals, locals+num, [&](expr const & l) {
+                return static_cast<bool>(m_mctx.get_metavar_decl(mvar)->get_context().get_local_decl(l)); }));
     buffer<expr> reverted;
     expr new_mvar = revert_core(num, locals, mvar, reverted);
     expr r = mk_app(new_mvar, reverted);