diff --git a/src/Lean/Meta/Constructions/CtorIdx.lean b/src/Lean/Meta/Constructions/CtorIdx.lean
index 8e66200962..a44e522220 100644
--- a/src/Lean/Meta/Constructions/CtorIdx.lean
+++ b/src/Lean/Meta/Constructions/CtorIdx.lean
@@ -79,17 +79,17 @@ public def mkCtorIdx (indName : Name) : MetaM Unit := do
       modifyEnv fun env => addProtected env declName
       setReducibleAttribute declName
 
-      -- Deprecated alias
-      -- (Add deprecation attribute after stage0 update)
-      let aliasName := mkToCtorIdxName indName
-      addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
-        (name        := aliasName)
-        (levelParams := info.levelParams)
-        (type        := declType)
-        (value       := mkConst declName us)
-        (hints       := ReducibilityHints.abbrev)
-      ))
-      modifyEnv fun env => addToCompletionBlackList env aliasName
-      modifyEnv fun env => addProtected env aliasName
-      setReducibleAttribute aliasName
-      Lean.Linter.setDeprecated aliasName { newName? := some declName, since? := "2025-08-25" }
+      -- Deprecated alias for enumeration types (which used to have `toCtorIdx`)
+      if (← isEnumType indName) then
+        let aliasName := mkToCtorIdxName indName
+        addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
+          (name        := aliasName)
+          (levelParams := info.levelParams)
+          (type        := declType)
+          (value       := mkConst declName us)
+          (hints       := ReducibilityHints.abbrev)
+        ))
+        modifyEnv fun env => addToCompletionBlackList env aliasName
+        modifyEnv fun env => addProtected env aliasName
+        setReducibleAttribute aliasName
+        Lean.Linter.setDeprecated aliasName { newName? := some declName, since? := "2025-08-25" }
diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out
index 12f77c85b6..8bfb81fad1 100644
--- a/tests/lean/computedFieldsCode.lean.expected.out
+++ b/tests/lean/computedFieldsCode.lean.expected.out
@@ -26,14 +26,6 @@
       let x_2 : tobj := Exp.ctorIdx x_1;
       dec x_1;
       ret x_2
-[Compiler.IR] [result]
-    def Exp.toCtorIdx (x_1 : @& tobj) : tobj :=
-      let x_2 : tobj := Exp.ctorIdx x_1;
-      ret x_2
-    def Exp.toCtorIdx._boxed (x_1 : tobj) : tobj :=
-      let x_2 : tobj := Exp.toCtorIdx x_1;
-      dec x_1;
-      ret x_2
 [Compiler.IR] [result]
     def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
       case x_1 : tobj of
diff --git a/tests/lean/run/ctorIdx.lean b/tests/lean/run/ctorIdx.lean
index edafffdb71..dd5afede2f 100644
--- a/tests/lean/run/ctorIdx.lean
+++ b/tests/lean/run/ctorIdx.lean
@@ -69,3 +69,14 @@ inductive Eq' : α → α → Prop where | refl (a : α) : Eq' a a
 /-- error: Unknown constant `Eq'.ctorIdx` -/
 #guard_msgs in
 #print Eq'.ctorIdx
+
+
+set_option linter.deprecated true
+
+-- Enumeration types get a deprecated alias, other types dont
+/-- info: Enum.toCtorIdx : Enum → Nat -/
+#guard_msgs in #check Enum.toCtorIdx
+/-- warning: `Enum.toCtorIdx` has been deprecated: Use `Enum.ctorIdx` instead -/
+#guard_msgs in example := Enum.toCtorIdx
+/-- error: Unknown identifier `Nonrec.toCtorIdx` -/
+#guard_msgs in #check Nonrec.toCtorIdx