diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 51c2892da46839fc5308a3ad1cffdfe05dafb44a..85df428322e515b911e47da80d24912e3615484a 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -98,7 +98,7 @@ Notation savedPredG Σ A := (savedAnythingG Σ (A -d> ▶ ∙)).
 Notation savedPredΣ A := (savedAnythingΣ (A -d> ▶ ∙)).
 
 Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
-  saved_anything_own (F := A -d> ▶ ∙) γ (OfeMor Next ∘ Φ).
+  saved_anything_own (F := A -d> ▶ ∙) γ (Next ∘ Φ).
 
 Global Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
   Contractive (saved_pred_own γ : (A -d> iPropO Σ) → iProp Σ).