diff --git a/tests/lean/run/coe13.lean b/tests/lean/run/coe13.lean
index 90a559081a..530470c332 100644
--- a/tests/lean/run/coe13.lean
+++ b/tests/lean/run/coe13.lean
@@ -21,10 +21,9 @@ check g (functor.to_fun f) 0
 
 check g f 0
 
-definition id (A : Type) (a : A) := a
 
 constant S : struct
 constant a : S
 
-check id (struct.to_sort S) a
-check id S a
+check @id (struct.to_sort S) a
+check @id S a
diff --git a/tests/lean/run/contra1.lean b/tests/lean/run/contra1.lean
index d90ade7791..bacc9b0a5e 100644
--- a/tests/lean/run/contra1.lean
+++ b/tests/lean/run/contra1.lean
@@ -9,8 +9,6 @@ by contradiction
 example : ∀ (a b : nat), (0:nat) = 1 → a = b :=
 by contradiction
 
-definition id {A : Type} (a : A) := a
-
 example : ∀ (a b : nat), id false → a = b :=
 by contradiction
 
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index 703a589060..296c2d453c 100644
--- a/tests/lean/run/div2.lean
+++ b/tests/lean/run/div2.lean
@@ -1,6 +1,6 @@
 import logic data.nat.sub algebra.relation data.prod
 
-open nat relation relation.iff_ops prod
+open nat relation prod
 open decidable
 open eq.ops
 
diff --git a/tests/lean/run/rel.lean b/tests/lean/run/rel.lean
deleted file mode 100644
index 0a78b06eb9..0000000000
--- a/tests/lean/run/rel.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-import logic algebra.relation
-open relation
-
-namespace is_equivalence
-  inductive cls {T : Type} (R : T → T → Prop) : Prop :=
-  mk : is_reflexive R → is_symmetric R → is_transitive R → cls R
-
-end is_equivalence
-
-theorem and_inhabited_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
-iff.intro (take Hab, and.elim_right Hab) (take Hb, and.intro Ha Hb)
-
-theorem test (a b c : Prop) (P : Prop → Prop) (H1 : a ↔ b) (H2 : c ∧ a) : c ∧ b :=
-iff.subst H1 H2
-
-theorem test2 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : Q ↔ (S ∧ Q) :=
-iff.symm (and_inhabited_left Q H1)
-
-theorem test3 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : R ↔ (S ∧ Q) :=
-iff.subst (test2 Q R S H3 H1) H3
-
-theorem test4 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : R ↔ (S ∧ Q) :=
-iff.subst (iff.symm (and_inhabited_left Q H1)) H3
diff --git a/tests/lean/run/section2.lean b/tests/lean/run/section2.lean
index de2964a5ca..c825d23bdb 100644
--- a/tests/lean/run/section2.lean
+++ b/tests/lean/run/section2.lean
@@ -2,9 +2,7 @@ import data.nat
 
 section foo
   variable A : Type
-  definition id (a : A) := a
   variable a : nat
-  check _root_.id nat a
 end foo
 
 namespace n1
diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean
index e5a3a39e10..4a333dc407 100644
--- a/tests/lean/run/tactic4.lean
+++ b/tests/lean/run/tactic4.lean
@@ -1,7 +1,6 @@
 import logic
 open tactic (renaming id->id_tac)
 
-definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A
 := by unfold id; assumption
diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean
index 41387388e6..8bb70744fa 100644
--- a/tests/lean/run/tactic5.lean
+++ b/tests/lean/run/tactic5.lean
@@ -1,8 +1,6 @@
 import logic
 open tactic (renaming id->id_tac)
 
-definition id {A : Type} (a : A) := a
-
 infixl `;`:15 := tactic.and_then
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A
diff --git a/tests/lean/run/tactic6.lean b/tests/lean/run/tactic6.lean
index e5a3a39e10..8a12e820f0 100644
--- a/tests/lean/run/tactic6.lean
+++ b/tests/lean/run/tactic6.lean
@@ -1,8 +1,6 @@
 import logic
 open tactic (renaming id->id_tac)
 
-definition id {A : Type} (a : A) := a
-
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A
 := by unfold id; assumption
 
diff --git a/tests/lean/run/vars_anywhere.lean b/tests/lean/run/vars_anywhere.lean
index b7dd0179be..6c80908a83 100644
--- a/tests/lean/run/vars_anywhere.lean
+++ b/tests/lean/run/vars_anywhere.lean
@@ -1,7 +1,5 @@
 variable {A : Type}
 
-definition id (a : A) := a
-
 check @id
 
 inductive list :=