diff --git a/Mathlib/Tactic/ToFun.lean b/Mathlib/Tactic/ToFun.lean
index fab5692165ec25..d96e3ed0a001f8 100644
--- a/Mathlib/Tactic/ToFun.lean
+++ b/Mathlib/Tactic/ToFun.lean
@@ -53,7 +53,7 @@ def toFunImpl (src : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Name :=
     if name == src.appendBefore "fun_" then
       logWarningAt id m!"`to_fun` correctly autogenerated the provided name `{.ofConstName name}`.\
         \nYou may remove it."
-  MetaM.run' <| addRelatedDecl src name tk optAttr
+  MetaM.run' <| addRelatedDecl src name (id.elim tk (·.raw)) optAttr
     (docstringPrefix? := s!"Eta-expanded form of `{src}`") (hoverInfo := true)
     fun value levels => do
     let type ← inferType value