From 5d1dfc3ec826069dcc34be0a0ed5bef5d476ff8f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 24 Jul 2024 12:19:32 +0200
Subject: [PATCH] fix

---
 src/Lean/Elab/MutualDef.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 2b2b69825816..d1d1ba208327 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -378,6 +378,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
         -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
         -- leads to more section variables being included than necessary
         let val ← instantiateMVars val
+        let val ← mkLambdaFVars xs val
         unless header.type.hasSorry || val.hasSorry do
           for var in vars do
             unless header.type.containsFVar var.fvarId! || val.containsFVar var.fvarId! || (← vars.anyM (fun v => return (← v.fvarId!.getType).containsFVar var.fvarId!)) do
@@ -387,7 +388,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
               else
                 var
               logWarningAt header.ref m!"included section variable '{var}' is not used in '{header.declName}', consider excluding it"
-        mkLambdaFVars xs val
+        return val
     if let some snap := header.bodySnap? then
       snap.new.resolve <| some {
         diagnostics :=