diff --git a/src/Lean/Elab/ComputedFields.lean b/src/Lean/Elab/ComputedFields.lean
index f07f4f23b3..0f8299e38d 100644
--- a/src/Lean/Elab/ComputedFields.lean
+++ b/src/Lean/Elab/ComputedFields.lean
@@ -108,10 +108,12 @@ def overrideCasesOn : M Unit := do
           forallTelescope (← inferType minor) fun args _ => do
             mkLambdaFVars ((if ← isScalarField ctor then #[] else compFieldVars) ++ args)
               (← mkUnsafeCastTo constMotive (mkAppN minor args)))
+  let nameOverride := mkCasesOnName name ++ `_override
   addDecl <| .defnDecl { casesOn with
-    name := mkCasesOnName name ++ `_override
+    name := nameOverride
+    all  := [nameOverride]
     value
-    hints := .opaque
+    hints  := .opaque
     safety := .unsafe
   }
   setInlineAttribute (mkCasesOnName name ++ `_override)