diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 85b6d2bdb3..bcd9ac8951 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -62,25 +62,4 @@ theorem length_firstn
                               ... = min (succ n) (succ (length l))
                                      : eq.symm (nat.min_succ_succ  n (length l))
 
-/- decidable -/
-
-definition has_decidable_eq [h : decidable_eq α]
-: ∀ (x y : list α), decidable (x = y)
-| nil nil := is_true rfl
-| nil (cons b s) := is_false (λ q, list.no_confusion q)
-| (cons a r) nil := is_false (λ q, list.no_confusion q)
-| (cons a r) (cons b s) :=
-  match h a b with
-  | (is_true h₁) :=
-    match has_decidable_eq r s with
-    | (is_true  h₂) :=
-       is_true (calc a :: r = b :: r : congr_arg (λc, c :: r) h₁
-                        ... = b :: s : congr_arg (λt, b :: t) h₂)
-    | (is_false h₂) :=
-      is_false (λ q, list.no_confusion q (λ heq teq, h₂ teq))
-    end
-  | (is_false h₁) :=
-     is_false (λ q, list.no_confusion q (λ heq teq, h₁ heq))
-  end
-
 end list
diff --git a/library/data/tuple.lean b/library/data/tuple.lean
index e4feb7f9b3..671eb9256c 100644
--- a/library/data/tuple.lean
+++ b/library/data/tuple.lean
@@ -47,14 +47,6 @@ theorem tail_cons (a : α) : Π (v : tuple α n), tail (a :: v) = v
 
 definition to_list : tuple α n → list α | ⟨ l, h ⟩ := l
 
-definition has_decidable_eq [decidable_eq α] {n:ℕ}
-  : ∀ (x y : tuple α n), decidable (x = y)
-| ⟨s,p⟩ ⟨t,q⟩ :=
-  match list.has_decidable_eq s t with
-  | (is_true h)  := is_true (subtype.eq h)
-  | (is_false h) := is_false (λr, subtype.no_confusion r (λleq (peq : p == q), h leq))
-  end
-
 /- append -/
 
 definition append {n m : nat} : tuple α n → tuple α m → tuple α (n + m)
@@ -129,7 +121,3 @@ section accum
 
 end accum
 end tuple
-
-instance decide_tuple_eq {A:Type.{1}} [decidable_eq A] {n:ℕ}
-  : ∀ {x y : tuple A n}, decidable (x = y)
-  := tuple.has_decidable_eq