diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean
index 33c82ded5c..d921b7f245 100644
--- a/src/Init/Lean/Elab/TermApp.lean
+++ b/src/Init/Lean/Elab/TermApp.lean
@@ -231,8 +231,8 @@ private def addLValArg (ref : Syntax) (baseName : Name) (fullName : Name) (e : E
     | some idx => do
       let namedArgs := namedArgs.eraseIdx idx;
       addLValArg i namedArgs b
-    | none =>
-      if d.isAppOf baseName then
+    | none => do
+      if d.consumeMData.isAppOf baseName then
         pure $ args.insertAt i (Arg.expr e)
       else if i < args.size then
         addLValArg (i+1) namedArgs b
diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index 139dee2987..5a7a791de9 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -541,6 +541,10 @@ def letName! : Expr → Name
 | letE n _ _ _ _ => n
 | _              => panic! "let expression expected"
 
+def consumeMData : Expr → Expr
+| mdata _ e _ => consumeMData e
+| e           => e
+
 def hasLooseBVars (e : Expr) : Bool :=
 e.looseBVarRange > 0
 
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index fc8cca9165..9b20e63777 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -177,3 +177,4 @@ f a
 #eval run "universes u v #check Type (max u v)"
 #eval run "#check 'a'"
 #eval fail "#check #['a', \"hello\"]"
+#eval run "#check fun (a : Array Nat) => a.size"