diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 9e54c625d0..6ccfeaab38 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -757,7 +757,7 @@ constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Arra
 @[extern "lean_expr_instantiate_rev_range"]
 constant instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr
 
-/-- Replace free variables `xs` with loose bound variables. -/
+/-- Replace free (or meta) variables `xs` with loose bound variables. -/
 @[extern "lean_expr_abstract"]
 constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr
 
diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index babeae0756..65c13cb023 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -39,19 +39,23 @@ expr abstract(expr const & e, name const & n) {
 static object * lean_expr_abstract_core(object * e0, size_t n, object * subst) {
     lean_assert(n <= lean_array_size(subst));
     expr const & e = reinterpret_cast<expr const &>(e0);
-    if (!has_fvar(e)) {
+    if (!has_fvar(e) && !has_mvar(e)) {
         lean_inc(e0);
         return e0;
     }
     expr r = replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
-            if (!has_fvar(m))
-                return some_expr(m); // expression m does not contain free variables
-            if (is_fvar(m)) {
+            if (!has_fvar(m) && !has_mvar(m))
+                return some_expr(m); // expression m does not contain free/meta variables
+            bool fv = is_fvar(m);
+            bool mv = is_mvar(m);
+            if (fv || mv) {
                 size_t i = n;
                 while (i > 0) {
                     --i;
                     object * v = lean_array_get_core(subst, i);
-                    if (is_fvar_core(v) && fvar_name_core(v) == fvar_name(m))
+                    if (fv && is_fvar_core(v) && fvar_name_core(v) == fvar_name(m))
+                        return some_expr(mk_bvar(offset + n - i - 1));
+                    if (mv && is_mvar_core(v) && mvar_name_core(v) == mvar_name(m))
                         return some_expr(mk_bvar(offset + n - i - 1));
                 }
                 return none_expr();
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 9e32e65685..3d15b3dc5c 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -145,6 +145,7 @@ struct expr_pair_eq {
 static expr_kind expr_kind_core(object * o) { return static_cast<expr_kind>(cnstr_tag(o)); }
 inline bool is_bvar(expr const & e)        { return e.kind() == expr_kind::BVar; }
 inline bool is_fvar_core(object * o)       { return expr_kind_core(o) == expr_kind::FVar; }
+inline bool is_mvar_core(object * o)       { return expr_kind_core(o) == expr_kind::MVar; }
 inline bool is_fvar(expr const & e)        { return e.kind() == expr_kind::FVar; }
 inline bool is_const(expr const & e)       { return e.kind() == expr_kind::Const; }
 inline bool is_mvar(expr const & e)        { return e.kind() == expr_kind::MVar; }
@@ -217,6 +218,7 @@ inline bool            is_bvar(expr const & e, unsigned i)   { return is_bvar(e)
 inline name const &    fvar_name_core(object * o)            { lean_assert(is_fvar_core(o)); return static_cast<name const &>(cnstr_get_ref(o, 0)); }
 inline name const &    fvar_name(expr const & e)             { lean_assert(is_fvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
 inline level const &   sort_level(expr const & e)            { lean_assert(is_sort(e)); return static_cast<level const &>(cnstr_get_ref(e, 0)); }
+inline name const &    mvar_name_core(object * o)            { lean_assert(is_mvar_core(o)); return static_cast<name const &>(cnstr_get_ref(o, 0)); }
 inline name const &    mvar_name(expr const & e)             { lean_assert(is_mvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
 inline name const &    const_name(expr const & e)            { lean_assert(is_const(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
 inline levels const &  const_levels(expr const & e)          { lean_assert(is_const(e)); return static_cast<levels const &>(cnstr_get_ref(e, 1)); }
diff --git a/tests/lean/run/abstractExpr.lean b/tests/lean/run/abstractExpr.lean
new file mode 100644
index 0000000000..155d05bae8
--- /dev/null
+++ b/tests/lean/run/abstractExpr.lean
@@ -0,0 +1,13 @@
+import Lean
+open Lean
+open Lean.Meta
+
+def test : MetaM Unit := do
+  let x ← mkFreshExprMVar (mkConst ``Nat)
+  let y ← mkFreshExprMVar (mkConst ``Nat)
+  let add := mkConst ``Nat.add
+  let e := mkApp3 add x (mkNatLit 1) y
+  IO.println (e.abstract #[x, y])
+  assert! e.abstract #[x, y] == mkApp3 add (mkBVar 1) (mkNatLit 1) (mkBVar 0)
+
+#eval test