diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 6f3a9100c4..61aa683a96 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -172,6 +172,7 @@ int main() {
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
+    initialize_library_core_module();
     initialize_library_module();
     init_default_print_fn();
     tst1();
@@ -179,6 +180,7 @@ int main() {
     environment_id_tester::tst1();
     environment_id_tester::tst2();
     finalize_library_module();
+    finalize_library_core_module();
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 766947f855..9f12ec840f 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -381,6 +381,7 @@ int main() {
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
+    initialize_library_core_module();
     initialize_library_module();
     init_default_print_fn();
     lean_assert(sizeof(expr) == sizeof(optional<expr>));
@@ -412,6 +413,7 @@ int main() {
     std::cout << "sizeof(std::function):   " << sizeof(std::function<expr(expr const &, optional<expr> const &)>) << "\n";
     std::cout << "done" << "\n";
     finalize_library_module();
+    finalize_library_core_module();
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();
diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp
index dcef2cb643..43b5f4c4f0 100644
--- a/src/tests/kernel/level.cpp
+++ b/src/tests/kernel/level.cpp
@@ -70,10 +70,12 @@ int main() {
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
+    initialize_library_core_module();
     initialize_library_module();
     tst1();
     tst2();
     finalize_library_module();
+    finalize_library_core_module();
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();
diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp
index 16fe929e7e..73f95d4872 100644
--- a/src/tests/kernel/max_sharing.cpp
+++ b/src/tests/kernel/max_sharing.cpp
@@ -67,6 +67,7 @@ int main() {
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
+    initialize_library_core_module();
     initialize_library_module();
     init_default_print_fn();
     {
@@ -76,6 +77,7 @@ int main() {
         tst3();
     }
     finalize_library_module();
+    finalize_library_core_module();
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index 86111f6908..fcee76c12c 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -160,6 +160,7 @@ int main() {
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
+    initialize_library_core_module();
     initialize_library_module();
     init_default_print_fn();
     tst1();
@@ -167,6 +168,7 @@ int main() {
     tst3();
     tst4();
     finalize_library_module();
+    finalize_library_core_module();
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();
diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt
index a333d08016..fdda3170ed 100644
--- a/src/tests/library/CMakeLists.txt
+++ b/src/tests/library/CMakeLists.txt
@@ -8,9 +8,6 @@ add_test(deep_copy "${CMAKE_CURRENT_BINARY_DIR}/deep_copy")
 add_executable(occurs occurs.cpp ${library_tst_objs})
 target_link_libraries(occurs ${EXTRA_LIBS})
 add_test(occurs "${CMAKE_CURRENT_BINARY_DIR}/occurs")
-add_executable(unifier unifier.cpp ${library_tst_objs})
-target_link_libraries(unifier ${EXTRA_LIBS})
-add_test(unifier "${CMAKE_CURRENT_BINARY_DIR}/unifier")
 add_executable(head_map head_map.cpp ${library_tst_objs})
 target_link_libraries(head_map ${EXTRA_LIBS})
 add_test(head_map "${CMAKE_CURRENT_BINARY_DIR}/head_map")
diff --git a/src/tests/library/deep_copy.cpp b/src/tests/library/deep_copy.cpp
index dfa2c6d9e5..c1897ce61a 100644
--- a/src/tests/library/deep_copy.cpp
+++ b/src/tests/library/deep_copy.cpp
@@ -33,9 +33,11 @@ int main() {
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
+    initialize_library_core_module();
     initialize_library_module();
     tst1();
     finalize_library_module();
+    finalize_library_core_module();
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();
diff --git a/src/tests/library/head_map.cpp b/src/tests/library/head_map.cpp
index d412335754..7852a39cdf 100644
--- a/src/tests/library/head_map.cpp
+++ b/src/tests/library/head_map.cpp
@@ -62,9 +62,11 @@ int main() {
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
+    initialize_library_core_module();
     initialize_library_module();
     tst1();
     finalize_library_module();
+    finalize_library_core_module();
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();
diff --git a/src/tests/library/occurs.cpp b/src/tests/library/occurs.cpp
index 2e6f275c59..aa65d9c637 100644
--- a/src/tests/library/occurs.cpp
+++ b/src/tests/library/occurs.cpp
@@ -33,9 +33,11 @@ int main() {
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
+    initialize_library_core_module();
     initialize_library_module();
     tst1();
     finalize_library_module();
+    finalize_library_core_module();
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();
diff --git a/src/tests/library/unifier.cpp b/src/tests/library/unifier.cpp
deleted file mode 100644
index 0d6cb02dfe..0000000000
--- a/src/tests/library/unifier.cpp
+++ /dev/null
@@ -1,41 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/test.h"
-#include "util/init_module.h"
-#include "util/sexpr/init_module.h"
-#include "kernel/init_module.h"
-#include "library/init_module.h"
-#include "library/unifier.h"
-using namespace lean;
-
-static void tst1() {
-    environment env;
-    expr Type = mk_Type();
-    expr A  = Local("A", Type);
-    expr f  = Local("f", A >> (A >> A));
-    expr a  = Local("a", A);
-    expr b  = Local("b", A);
-    expr m  = mk_metavar("m", A);
-    expr t1 = mk_app(f, m, m);
-    expr t2 = mk_app(f, a, b);
-    auto r = unify(env, t1, t2);
-    lean_assert(!r.pull());
-}
-
-int main() {
-    save_stack_info();
-    initialize_util_module();
-    initialize_sexpr_module();
-    initialize_kernel_module();
-    initialize_library_module();
-    tst1();
-    finalize_library_module();
-    finalize_kernel_module();
-    finalize_sexpr_module();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/shell/file1.lean b/src/tests/shell/file1.lean
index 4b5f3cd01a..4c2183f59c 100644
--- a/src/tests/shell/file1.lean
+++ b/src/tests/shell/file1.lean
@@ -1,3 +1,4 @@
+import data.nat
 check nat
 check nat.add_zero
 check nat.zero_add
diff --git a/src/tests/shell/file2.lean b/src/tests/shell/file2.lean
index e6d356d2c6..26434a4a91 100644
--- a/src/tests/shell/file2.lean
+++ b/src/tests/shell/file2.lean
@@ -1,3 +1,4 @@
+import data.nat
 check nat
 check nat.add_zero
 check nat.zero_add
@@ -5,6 +6,4 @@ check nat.zero_add
 
 open nat
 example (a b : nat) : a = 0 → b = 0 → a = b :=
-begin
-  intros, substvars
-end
+assume h1 h2, eq.subst (eq.symm h1) (eq.subst (eq.symm h2) (eq.refl 0))