From 48b924fae26f0354625d65eb047c57d034945aa1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 20 Dec 2024 19:10:38 +0900
Subject: [PATCH] fix(frontend): Incorrect capture of binder term

---
 Pantograph/Frontend/Elab.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 3da5fca..a07efb0 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -106,7 +106,7 @@ structure InfoWithContext where
 
 private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
   let infos ← t.findAllInfoM none fun i ctx? => match i with
-    | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
+    | .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
       let .some ctx := ctx? | return (false, true)
       if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
         if expectedType?.isNone then