chore: use String.ofList instead of String.mk in elaborator+kernel

[TwoFX]

This PR is a follow-up to #11017, preparing for the eventual removal of the String.mk function.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3d307925b7b8d88f8cdbf94e951908a8383b8cea --onto 1ce05b2a179eac8a902995c0caddc609c0169c49. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-01 14:49:09)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3d307925b7b8d88f8cdbf94e951908a8383b8cea --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-01 14:49:11)