From ed754725e6caf035d819a5153105f64f2ca123c8 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 7 Aug 2022 18:37:17 +0200
Subject: [PATCH] fix: discriminant info tree term

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

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 35e545ec54..13f56d0cc0 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -62,7 +62,7 @@ private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
   | some e@(Expr.fvar fvarId) =>
     let localDecl ← fvarId.getDecl
     if !isAuxDiscrName localDecl.userName then
-      addTermInfo discr e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
+      addTermInfo term e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
     else
       instantiateMVars localDecl.value
   | _ => throwErrorAt discr "unexpected discriminant"