fix

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 :=