diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean
index 29fa7222d3..e4005dbcb4 100644
--- a/src/Init/Lean/MetavarContext.lean
+++ b/src/Init/Lean/MetavarContext.lean
@@ -532,7 +532,7 @@ partial def main : Expr → M Expr
         instArgs f
       else do
         newVal ← visit main val;
-        if newVal.hasMVar then
+        if newVal.hasExprMVar then
           instArgs f
         else do
           args ← args.mapM (visit main);