From 0cfdf285e3dbf4cf984325a62a8dc2792657a613 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 6 Nov 2022 17:15:47 -0800
Subject: [PATCH] chore: remove unnecessary auxiliary declaration

---
 src/Lean/Compiler/LCNF/Simp/Main.lean | 42 +++++++++++++--------------
 1 file changed, 20 insertions(+), 22 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean
index 377eec9421..5d255ccfa5 100644
--- a/src/Lean/Compiler/LCNF/Simp/Main.lean
+++ b/src/Lean/Compiler/LCNF/Simp/Main.lean
@@ -303,26 +303,24 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
     if let some k ← simpCasesOnCtor? c then
       return k
     else
-      let simpCasesDefault := do
-        let discr ← normFVar c.discr
-        let resultType ← normExpr c.resultType
-        markUsedFVar discr
-        let alts ← c.alts.mapMonoM fun alt => do
-          match alt with
-          | .alt ctorName ps k =>
-            if !(k matches .unreach ..) && (← ps.anyM fun p => isInductiveWithNoCtors p.type) then
-              let type ← k.inferType
-              eraseCode k
-              markSimplified
-              return alt.updateCode (.unreach type)
-            else
-              withDiscrCtor discr ctorName ps do
-                return alt.updateCode (← simp k)
-          | .default k => return alt.updateCode (← simp k)
-        let alts ← addDefaultAlt alts
-        if alts.size == 1 && alts[0]! matches .default .. then
-          return alts[0]!.getCode
-        else
-          return code.updateCases! resultType discr alts
-      simpCasesDefault
+      let discr ← normFVar c.discr
+      let resultType ← normExpr c.resultType
+      markUsedFVar discr
+      let alts ← c.alts.mapMonoM fun alt => do
+        match alt with
+        | .alt ctorName ps k =>
+          if !(k matches .unreach ..) && (← ps.anyM fun p => isInductiveWithNoCtors p.type) then
+            let type ← k.inferType
+            eraseCode k
+            markSimplified
+            return alt.updateCode (.unreach type)
+          else
+            withDiscrCtor discr ctorName ps do
+              return alt.updateCode (← simp k)
+        | .default k => return alt.updateCode (← simp k)
+      let alts ← addDefaultAlt alts
+      if alts.size == 1 && alts[0]! matches .default .. then
+        return alts[0]!.getCode
+      else
+        return code.updateCases! resultType discr alts
 end