diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean
index 22da79de4a..012cf614f8 100644
--- a/library/init/control/combinators.lean
+++ b/library/init/control/combinators.lean
@@ -54,13 +54,9 @@ def mmap {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α 
 | (h :: t) := do h' ← f h, t' ← mmap t, pure (h' :: t')
 
 @[specialize]
-def mmap' {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
+def mfor {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
 | []       := pure ⟨⟩
-| (h :: t) := f h *> mmap' t
-
-@[specialize]
-def mfor {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit :=
-List.mmap' f
+| (h :: t) := f h *> mfor t
 
 @[specialize]
 def mfilter {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → m (List α)
diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 9ea22928f9..52a95ebb21 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -856,7 +856,7 @@ def setOption.elaborate : Elaborator :=
 def noKind.elaborate : Elaborator := λ stx, do
   some n ← pure stx.asNode
     | error stx "noKind.elaborate: unreachable",
-  n.args.mmap' command.elaborate
+  n.args.mfor command.elaborate
 
 def end.elaborate : Elaborator :=
 λ cmd, do