From f28a7306f24dfef3ce0b91bbfc214f1b7cee4ad4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Nov 2020 10:53:47 -0800
Subject: [PATCH] fix: append `match_<idx>` suffix only there is more than one
 alternative

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

diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index 9e5f431afe..e93cecbae9 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -23,7 +23,8 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
       pure alt
     else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
       let s ← get
-      let holeName := mkIdentFrom holeOrTacticSeq (parentTag ++ (`match).appendIndexAfter s.nextIdx)
+      let tag := if alts.size > 1 then parentTag ++ (`match).appendIndexAfter s.nextIdx else parentTag
+      let holeName := mkIdentFrom holeOrTacticSeq tag
       let newHole ← `(?$holeName:ident)
       modify fun s => { s with nextIdx := s.nextIdx + 1}
       pure $ alt.setArg 2 newHole