diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 8d854b1b1a..95d0c38af5 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -96,7 +96,7 @@ private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHe
     let newHeader ← withRef view.ref do
       let ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
       applyAttributesAt declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration
-      withAutoBoundImplicitLocal <| withLevelNames levelNames <|
+      withDeclName declName <| withAutoBoundImplicitLocal <| withLevelNames levelNames <|
         elabBinders (catchAutoBoundImplicit := true) view.binders.getArgs fun xs => do
           let refForElabFunType := view.value
           elabFunType refForElabFunType xs view fun xs type => do
diff --git a/tests/lean/run/missingDeclName.lean b/tests/lean/run/missingDeclName.lean
new file mode 100644
index 0000000000..c71f884c30
--- /dev/null
+++ b/tests/lean/run/missingDeclName.lean
@@ -0,0 +1 @@
+def foo {α β : Type} (xs : Array (α × β)) (H : true = xs.all fun (x, y) => true) : Unit := ()