diff --git a/src/Init/Lean/Util/WHNF.lean b/src/Init/Lean/Util/WHNF.lean
index 109e95b1d8..149b175c0a 100644
--- a/src/Init/Lean/Util/WHNF.lean
+++ b/src/Init/Lean/Util/WHNF.lean
@@ -288,7 +288,7 @@ else
     f' ← whnfCore f;
     if f'.isLambda then
       let revArgs := e.getAppRevArgs;
-      whnfCore $ f.betaRev revArgs
+      whnfCore $ f'.betaRev revArgs
     else do
       let done : Unit → m Expr := fun _ =>
         if f == f' then pure e else pure $ e.updateFn f';