From 438494ae3fab68bdb13af1a625ccb06b2daf69ba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Nov 2020 06:22:46 -0800
Subject: [PATCH] chore: fix assertion

---
 src/kernel/abstract.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index 9320f11878..8130fed942 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 expr abstract(expr const & e, unsigned n, expr const * subst) {
-    lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return !has_loose_bvars(e) && is_local_or_fvar(e); }));
+    lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return !has_loose_bvars(e) && is_fvar(e); }));
     if (!has_fvar(e))
         return e;
     return replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {