From da24708ba58ff1fc9d49eca417a82b7b4e3206c3 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 19 Feb 2024 10:24:11 +0100
Subject: [PATCH] refactor: use isAppOfArity (#3394)

---
 src/Lean/Meta/Tactic/Split.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 18f65c2297..6a48b1d2d8 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -119,7 +119,7 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N
       let foundRef ← IO.mkRef false
       let rec mkNewTarget (e : Expr) : MetaM Expr := do
         let pre (e : Expr) : MetaM TransformStep := do
-          if !e.isAppOf matcherDeclName || e.getAppNumArgs != matcherInfo.arity then
+          if !e.isAppOfArity matcherDeclName matcherInfo.arity then
             return .continue
           let some matcherApp ← matchMatcherApp? e | return .continue
           for matcherDiscr in matcherApp.discrs, discr in discrs do