diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 95c37c11f..378f3fe2a 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -785,7 +785,7 @@ public:
         } else {
             b = ensure_type(visit_expecting_type(b));
         }
-        b = abstract(b, l);
+        b = abstract_local(b, l);
         return update_binding(e, d, b);
     }
 
@@ -799,7 +799,7 @@ public:
         } else {
             b = visit(b);
         }
-        b = abstract(b, l);
+        b = abstract_local(b, l);
         return update_binding(e, d, b);
     }