From 3586337c567f97d9bebd6eba131e08f037441e03 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Sep 2020 18:55:13 -0700
Subject: [PATCH] perf: handle easy case efficiently

---
 src/Lean/Meta/KAbstract.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/KAbstract.lean b/src/Lean/Meta/KAbstract.lean
index 9ea5623f51..065c32452e 100644
--- a/src/Lean/Meta/KAbstract.lean
+++ b/src/Lean/Meta/KAbstract.lean
@@ -35,7 +35,10 @@ private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : Hea
     visitChildren ()
 
 def kabstract {m} [MonadLiftT MetaM m] (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : m Expr := liftMetaM do
-(kabstractAux occs p p.toHeadIndex p.headNumArgs e 0).run' 1
+if p.isFVar && occs == Occurrences.all then
+  pure $ e.abstract #[p] -- Easy case
+else
+  (kabstractAux occs p p.toHeadIndex p.headNumArgs e 0).run' 1
 
 end Meta
 end Lean