diff --git a/src/Lean/Meta/Constructions/CtorIdx.lean b/src/Lean/Meta/Constructions/CtorIdx.lean
index 3a32ca6ead..b23f3c2289 100644
--- a/src/Lean/Meta/Constructions/CtorIdx.lean
+++ b/src/Lean/Meta/Constructions/CtorIdx.lean
@@ -72,17 +72,13 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
             value := mkApp value alt
           pure value
         mkLambdaFVars (xs.push x) value
-      let decl := .defnDecl (← mkDefinitionValInferringUnsafe
+      addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
         (name        := declName)
         (levelParams := info.levelParams)
         (type        := declType)
         (value       := declValue)
         (hints       := ReducibilityHints.abbrev)
-      )
-      addDecl decl
-      if info.numCtors = 1 then
-        setInlineAttribute declName .macroInline
-      compileDecl decl
+      ))
       modifyEnv fun env => addToCompletionBlackList env declName
       modifyEnv fun env => addProtected env declName
       setReducibleAttribute declName
@@ -90,16 +86,13 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
       -- Deprecated alias for enumeration types (which used to have `toCtorIdx`)
       if (← isEnumType indName) then
         let aliasName := mkToCtorIdxName indName
-        let decl := .defnDecl (← mkDefinitionValInferringUnsafe
+        addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
           (name        := aliasName)
           (levelParams := info.levelParams)
           (type        := declType)
           (value       := mkConst declName us)
           (hints       := ReducibilityHints.abbrev)
-        )
-        addDecl decl
-        setInlineAttribute aliasName .macroInline
-        compileDecl decl
+        ))
         modifyEnv fun env => addToCompletionBlackList env aliasName
         modifyEnv fun env => addProtected env aliasName
         setReducibleAttribute aliasName