diff --git a/RELEASES.md b/RELEASES.md
index cb62720247..b1e5936d15 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -132,6 +132,8 @@ fact.def :
 
 * The change to the instance name algorithm (described above) can break projects that made use of the auto-generated names.
 
+* `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed.
+
 v4.7.0
 ---------
 
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index 86a1e5a3bf..e6344f0320 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -13,10 +13,14 @@ namespace Option
 deriving instance DecidableEq for Option
 deriving instance BEq for Option
 
-def toMonad [Monad m] [Alternative m] : Option α → m α
+/-- Lifts an optional value to any `Alternative`, sending `none` to `failure`. -/
+def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
+@[deprecated getM] def toMonad [Monad m] [Alternative m] : Option α → m α :=
+  getM
+
 @[inline] def toBool : Option α → Bool
   | some _ => true
   | none   => false