diff --git a/library/Init/Data/Nat/Control.lean b/library/Init/Data/Nat/Control.lean
index 334d285715..5bf22ab9bc 100644
--- a/library/Init/Data/Nat/Control.lean
+++ b/library/Init/Data/Nat/Control.lean
@@ -36,7 +36,7 @@ foldMAux f n n a
 | 0,   a => pure a
 | i+1, a => f i a >>= foldRevMAux i
 
-@[inline] def mfoldRev {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
+@[inline] def foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
 foldRevMAux f n a
 
 end Nat