diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index 12120bb764..f14c7731e3 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -132,10 +132,6 @@ theorem length_map₂ : ∀(f : A → B → C) x y, length (map₂ f x y) = min
       ... = min (length (xh::xr)) (length (yh::yr))   : rfl
 
 /- filter -/
-definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
-| []     := []
-| (a::l) := if p a then a :: filter l else filter l
-
 theorem filter_nil [simp] (p : A → Prop) [h : decidable_pred p] : filter p [] = [] := rfl
 
 theorem filter_cons_of_pos [simp] {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ l, p a → filter p (a::l) = a :: filter p l :=
diff --git a/library/init/list.lean b/library/init/list.lean
index 4e00d9be69..183cedcc4b 100644
--- a/library/init/list.lean
+++ b/library/init/list.lean
@@ -65,6 +65,10 @@ definition map {B : Type} (f : A → B) : list A → list B
 definition join : list (list A) → list A
 | []        := []
 | (l :: ls) := append l (join ls)
+
+definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
+| []     := []
+| (a::l) := if p a then a :: filter l else filter l
 end list
 
 definition list_has_append [instance] {A : Type} : has_append (list A) :=