diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 8b988c646d..168c5ca91f 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -253,9 +253,7 @@ unfold : ∀ (P : ℕ → Set b)
          (f : ∀ {n} → P (suc n) → Maybe (A × P n)) →
          ∀ {n} → P n → List A
 unfold P f {n = zero}  s = []
-unfold P f {n = suc n} s with f s
-... | nothing       = []
-... | just (x , s′) = x ∷ unfold P f s′
+unfold P f {n = suc n} s = maybe′ (λ (x , s′) → x ∷ unfold P f s′) [] (f s)
 
 ------------------------------------------------------------------------
 -- Operations for reversing lists