diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 5654a45cab..79ab6c4859 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -144,10 +144,6 @@ rfl
 theorem head_append [simp] [h : inhabited T] (t : list T) : ∀ {s : list T}, s ≠ [] → head (s ++ t) = head s :=
 sorry -- by rec_inst_simp
 
-definition tail : list T → list T
-| []       := []
-| (a :: l) := l
-
 theorem tail_nil [simp] : tail (@nil T) = [] :=
 rfl
 
diff --git a/library/init/list.lean b/library/init/list.lean
index 67fe278605..9cd8a9aecd 100644
--- a/library/init/list.lean
+++ b/library/init/list.lean
@@ -49,4 +49,8 @@ definition nth : list A → nat → option A
 | (a :: l) 0     := some a
 | (a :: l) (n+1) := nth l n
 
+definition tail : list A → list A
+| []       := []
+| (a :: l) := l
+
 end list