diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 64cde873eb..5ef159ea97 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -226,11 +226,6 @@ abbrev TermElab  := Syntax → Option Expr → TermElabM Expr
 /-
 Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 whole monad stack at every use site. May eventually be covered by `deriving`.
-
-TODO: this trick does not work in the old/new code generators anymore.
-TODO: figure out a way to instruct the compiler to optimize this code once,
-and then lambda lift all methods once. Perhaps, we should do it whenever the
-instance is marked as always_inline.
 -/
 @[always_inline]
 instance : Monad TermElabM :=