diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 02f6626502..3e5f20eca0 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -520,7 +520,8 @@ e ← withProj delab;
 -- not perfectly authentic: elaborates to the `idx`-th named projection
 -- function (e.g. `e.1` is `Prod.fst e`), which unfolds to the actual
 -- `proj`.
-`($(e).$(mkStxNumLitAux idx):fieldIdx)
+let idx := mkStxLit fieldIdxKind (toString (idx + 1));
+`($(e).$idx:fieldIdx)
 
 /-- Delaborate a call to a projection function such as `Prod.fst`. -/
 @[builtinDelab app]