diff --git a/tests/lean/print_thm.lean b/tests/lean/print_thm.lean
deleted file mode 100644
index 66dac3d5af..0000000000
--- a/tests/lean/print_thm.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-open nat
-
-theorem simple (a : nat) : a ≥ 0 :=
-zero_le a
-
-print simple
-
-reveal simple
-
-print simple
diff --git a/tests/lean/print_thm.lean.expected.out b/tests/lean/print_thm.lean.expected.out
deleted file mode 100644
index 0181442c38..0000000000
--- a/tests/lean/print_thm.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-theorem simple : ∀ (a : ℕ), a ≥ 0
-'simple' is still in the theorem queue, use command 'reveal simple' to access its definition.
-theorem simple : ∀ (a : ℕ), a ≥ 0 :=
-zero_le
diff --git a/tests/lean/unfold_crash2.lean b/tests/lean/unfold_crash2.lean
deleted file mode 100644
index abfe24e11d..0000000000
--- a/tests/lean/unfold_crash2.lean
+++ /dev/null
@@ -1,38 +0,0 @@
---
-open tactic
-
-inductive vector (A : Type) : nat → Type
-  | nil {} : vector 0
-  | cons : Π {n}, A -> vector n -> vector (nat.succ n)
-
-definition vmap {A B : Type} (f : A -> B) : Π {n}, vector A n -> vector B n
-| vmap vector.nil := vector.nil
-| vmap (vector.cons x xs) := vector.cons (f x) (vmap xs)
-
-definition vappend {A} : Π {n m}, vector A n -> vector A m -> vector A (m + n)
-| vappend vector.nil vector.nil := vector.nil
-| vappend vector.nil (vector.cons x xs) := vector.cons x xs
-| vappend (vector.cons x xs) vector.nil := vector.cons x (vappend xs vector.nil)
-| vappend (vector.cons x xs) (vector.cons y ys) := vector.cons x (vappend xs (vector.cons y ys))
-
-axiom Sorry : ∀ A, A
-
-theorem vappend_assoc :
-  Π {A : Type} {n m k : nat} (v1 : vector A n) (v2 : vector A m) (v3 : vector A k),
-  vappend (vappend v1 v2) v3 == vappend v1 (vappend v2 v3) :=
-by do
-     intros,
-     -- should not unfold anything since term does not contains any of the patterns above.
-     unfold [`vappend],
-     trace_state, trace "-----------",
-     get_local `v1 >>= cases,
-     trace_state, trace "-----------",
-     -- should not unfold anything since term does not contains any of the patterns above.
-     unfold [`vappend],
-     trace_state, trace "-----------",
-     get_local `v2 >>= cases,
-     trace_state, trace "-----------",
-     -- now it should unfold
-     unfold [`vappend],
-     trace_state, trace "-----------",
-     repeat $ mk_const `Sorry >>= apply
diff --git a/tests/lean/unfold_crash2.lean.expected.out b/tests/lean/unfold_crash2.lean.expected.out
deleted file mode 100644
index 00d290b8df..0000000000
--- a/tests/lean/unfold_crash2.lean.expected.out
+++ /dev/null
@@ -1,85 +0,0 @@
-A : Type,
-n m k : ℕ,
-v1 : vector A n,
-v2 : vector A m,
-v3 : vector A k
-⊢ vappend (vappend v1 v2) v3 == vappend v1 (vappend v2 v3)
------------
-A : Type,
-m k : ℕ,
-v2 : vector A m,
-v3 : vector A k,
-n : ℕ
-⊢ vappend (vappend vector.nil v2) v3 == vappend vector.nil (vappend v2 v3)
-
-A : Type,
-m k : ℕ,
-v2 : vector A m,
-v3 : vector A k,
-n n : ℕ,
-a : A,
-a : vector A n
-⊢ vappend (vappend (vector.cons a a_1) v2) v3 == vappend (vector.cons a a_1) (vappend v2 v3)
------------
-A : Type,
-m k : ℕ,
-v2 : vector A m,
-v3 : vector A k,
-n : ℕ
-⊢ vappend (vappend vector.nil v2) v3 == vappend vector.nil (vappend v2 v3)
-
-A : Type,
-m k : ℕ,
-v2 : vector A m,
-v3 : vector A k,
-n n : ℕ,
-a : A,
-a : vector A n
-⊢ vappend (vappend (vector.cons a a_1) v2) v3 == vappend (vector.cons a a_1) (vappend v2 v3)
------------
-A : Type,
-k : ℕ,
-v3 : vector A k,
-n m : ℕ
-⊢ vappend (vappend vector.nil vector.nil) v3 == vappend vector.nil (vappend vector.nil v3)
-
-A : Type,
-k : ℕ,
-v3 : vector A k,
-n m n : ℕ,
-a : A,
-a : vector A n
-⊢ vappend (vappend vector.nil (vector.cons a a_1)) v3 == vappend vector.nil (vappend (vector.cons a a_1) v3)
-
-A : Type,
-m k : ℕ,
-v2 : vector A m,
-v3 : vector A k,
-n n : ℕ,
-a : A,
-a : vector A n
-⊢ vappend (vappend (vector.cons a a_1) v2) v3 == vappend (vector.cons a a_1) (vappend v2 v3)
------------
-A : Type,
-k : ℕ,
-v3 : vector A k,
-n m : ℕ
-⊢ vappend vector.nil v3 == vappend vector.nil (vappend vector.nil v3)
-
-A : Type,
-k : ℕ,
-v3 : vector A k,
-n m n : ℕ,
-a : A,
-a : vector A n
-⊢ vappend (vappend vector.nil (vector.cons a a_1)) v3 == vappend vector.nil (vappend (vector.cons a a_1) v3)
-
-A : Type,
-m k : ℕ,
-v2 : vector A m,
-v3 : vector A k,
-n n : ℕ,
-a : A,
-a : vector A n
-⊢ vappend (vappend (vector.cons a a_1) v2) v3 == vappend (vector.cons a a_1) (vappend v2 v3)
------------