diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index b4fd1897d..624758d67 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
-for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
+for_each_fn.cpp replace_fn.cpp free_vars.cpp abstract.cpp
 instantiate.cpp context.cpp formatter.cpp max_sharing.cpp
 definition.cpp replace_visitor.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index d14674a21..6cffde8b2 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,4 +1,5 @@
-add_library(library deep_copy.cpp expr_lt.cpp)
+add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp
+  occurs.cpp)
 # io_state_stream.cpp
 # kernel_bindings.cpp
 # context_to_lambda.cpp placeholder.cpp
diff --git a/src/kernel/decl_macros.h b/src/library/decl_macros.h
similarity index 100%
rename from src/kernel/decl_macros.h
rename to src/library/decl_macros.h
diff --git a/src/kernel/io_state.cpp b/src/library/io_state.cpp
similarity index 97%
rename from src/kernel/io_state.cpp
rename to src/library/io_state.cpp
index 375f192b8..5bf587e97 100644
--- a/src/kernel/io_state.cpp
+++ b/src/library/io_state.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/io_state.h"
 #include "kernel/kernel_exception.h"
+#include "library/io_state.h"
 
 namespace lean {
 io_state::io_state(formatter const & fmt):
diff --git a/src/kernel/io_state.h b/src/library/io_state.h
similarity index 100%
rename from src/kernel/io_state.h
rename to src/library/io_state.h
diff --git a/src/kernel/occurs.cpp b/src/library/occurs.cpp
similarity index 94%
rename from src/kernel/occurs.cpp
rename to src/library/occurs.cpp
index 280965043..2c7c64a2f 100644
--- a/src/kernel/occurs.cpp
+++ b/src/library/occurs.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/occurs.h"
 #include "kernel/find_fn.h"
+#include "library/occurs.h"
 
 namespace lean {
 bool occurs(expr const & n, expr const & m) {
diff --git a/src/kernel/occurs.h b/src/library/occurs.h
similarity index 100%
rename from src/kernel/occurs.h
rename to src/library/occurs.h
diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt
index cabd1bd7b..cda8bfb0c 100644
--- a/src/tests/kernel/CMakeLists.txt
+++ b/src/tests/kernel/CMakeLists.txt
@@ -28,9 +28,6 @@ add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace)
 # target_link_libraries(environment ${EXTRA_LIBS})
 # add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment)
 # set_tests_properties(environment PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
-add_executable(occurs occurs.cpp)
-target_link_libraries(occurs ${EXTRA_LIBS})
-add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
 add_executable(metavar metavar.cpp)
 target_link_libraries(metavar ${EXTRA_LIBS})
 add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)
diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt
index bdd1c60e7..51b9b168d 100644
--- a/src/tests/library/CMakeLists.txt
+++ b/src/tests/library/CMakeLists.txt
@@ -7,6 +7,9 @@ add_test(expr_lt ${CMAKE_CURRENT_BINARY_DIR}/expr_lt)
 add_executable(deep_copy deep_copy.cpp)
 target_link_libraries(deep_copy ${EXTRA_LIBS})
 add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)
+add_executable(occurs occurs.cpp)
+target_link_libraries(occurs ${EXTRA_LIBS})
+add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
 # add_executable(arith_tst arith.cpp)
 # target_link_libraries(arith_tst ${EXTRA_LIBS})
 # add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)
diff --git a/src/tests/kernel/occurs.cpp b/src/tests/library/occurs.cpp
similarity index 95%
rename from src/tests/kernel/occurs.cpp
rename to src/tests/library/occurs.cpp
index a6927f8e1..d78d3f897 100644
--- a/src/tests/kernel/occurs.cpp
+++ b/src/tests/library/occurs.cpp
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/test.h"
-#include "kernel/occurs.h"
 #include "kernel/abstract.h"
+#include "library/occurs.h"
 using namespace lean;
 
 static void tst1() {