From e8c1647fa546cd2acdec7af0d3179627c6b5bf22 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Oct 2020 12:37:11 -0700
Subject: [PATCH] chore: improve condition

---
 src/Lean/Elab/PreDefinition/Structural.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index df0e3cfb62..ce1b50073e 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -245,7 +245,8 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
       let matcherApp? ← matchMatcherApp? e
       match matcherApp? with
       | some matcherApp =>
-        if !containsRecFn recFnName e then
+        /- If none of the alternatives contain a recursive application, we process it as a regular one. -/
+        if matcherApp.alts.all fun alt => !containsRecFn recFnName alt then
           processApp e
         else
           /- Here is an example we currently not handle