diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 7e0f5bd329..e5b9a27e9d 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -1267,7 +1267,7 @@ def getRevArg!' : Expr → Nat → Expr
   getRevArg! e (n - i - 1)
 
 /-- Similar to `getArg!`, but skips mdata -/
-@[inline] def getArg!' (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
+@[inline] def getArg!' (e : Expr) (i : Nat) (n := e.getAppNumArgs') : Expr :=
   getRevArg!' e (n - i - 1)
 
 /-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or returns `v₀` if out of bounds. -/
diff --git a/tests/lean/run/getArgPrime.lean b/tests/lean/run/getArgPrime.lean
new file mode 100644
index 0000000000..6a5481a002
--- /dev/null
+++ b/tests/lean/run/getArgPrime.lean
@@ -0,0 +1,11 @@
+import Lean.Expr
+
+open Lean Expr
+
+example :
+  getArg! (mkApp (.mdata .empty (mkApp (mkConst ``Nat.add) (mkNatLit 1))) (mkNatLit 2)) 0
+    = mkNatLit 2 := rfl
+
+example :
+  getArg!' (mkApp (.mdata .empty (mkApp (mkConst ``Nat.add) (mkNatLit 1))) (mkNatLit 2)) 0
+    = mkNatLit 1 := rfl