SimpTheorems.addDeclToUnfold vs mkSimpAttr

Stream: lean4

[Jannis Limperg]

I'm looking at docs4#Lean.Meta.SimpTheorems.addDeclToUnfold and docs4#Lean.Meta.mkSimpAttr. When applying a simp attribute to a definition, mkSimpAttr.add implements essentially the same logic as SimpTheorems.addDeclToUnfold, but it also has this line:

ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind

Afaict this has no equivalent in addDeclToUnfold. Is this discrepancy a bug?