diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cce65f841..e83ee090a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -76,7 +76,7 @@ include_directories(${LEAN_SOURCE_DIR}/util/sexpr)
 include_directories(${LEAN_SOURCE_DIR}/interval)
 include_directories(${LEAN_SOURCE_DIR}/kernel)
 include_directories(${LEAN_SOURCE_DIR}/kernel/arith)
-include_directories(${LEAN_SOURCE_DIR}/exprlib)
+include_directories(${LEAN_SOURCE_DIR}/library)
 include_directories(${LEAN_SOURCE_DIR}/parsers)
 include_directories(${LEAN_SOURCE_DIR}/frontends/lean)
 
@@ -92,8 +92,8 @@ add_subdirectory(kernel)
 set(LEAN_LIBS ${LEAN_LIBS} kernel)
 add_subdirectory(kernel/arith)
 set(LEAN_LIBS ${LEAN_LIBS} kernel_arith)
-add_subdirectory(exprlib)
-set(LEAN_LIBS ${LEAN_LIBS} exprlib)
+add_subdirectory(library)
+set(LEAN_LIBS ${LEAN_LIBS} library)
 add_subdirectory(frontends/lean)
 set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
diff --git a/src/exprlib/CMakeLists.txt b/src/exprlib/CMakeLists.txt
deleted file mode 100644
index f5d1802f7..000000000
--- a/src/exprlib/CMakeLists.txt
+++ /dev/null
@@ -1,3 +0,0 @@
-add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp
-  formatter.cpp context_to_lambda.cpp state.cpp)
-target_link_libraries(exprlib ${LEAN_LIBS})
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
new file mode 100644
index 000000000..9524b1da6
--- /dev/null
+++ b/src/library/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp
+  formatter.cpp context_to_lambda.cpp state.cpp)
+target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/exprlib/basic_thms.cpp b/src/library/basic_thms.cpp
similarity index 100%
rename from src/exprlib/basic_thms.cpp
rename to src/library/basic_thms.cpp
diff --git a/src/exprlib/basic_thms.h b/src/library/basic_thms.h
similarity index 100%
rename from src/exprlib/basic_thms.h
rename to src/library/basic_thms.h
diff --git a/src/exprlib/context_to_lambda.cpp b/src/library/context_to_lambda.cpp
similarity index 100%
rename from src/exprlib/context_to_lambda.cpp
rename to src/library/context_to_lambda.cpp
diff --git a/src/exprlib/context_to_lambda.h b/src/library/context_to_lambda.h
similarity index 100%
rename from src/exprlib/context_to_lambda.h
rename to src/library/context_to_lambda.h
diff --git a/src/exprlib/deep_copy.cpp b/src/library/deep_copy.cpp
similarity index 100%
rename from src/exprlib/deep_copy.cpp
rename to src/library/deep_copy.cpp
diff --git a/src/exprlib/deep_copy.h b/src/library/deep_copy.h
similarity index 100%
rename from src/exprlib/deep_copy.h
rename to src/library/deep_copy.h
diff --git a/src/exprlib/formatter.cpp b/src/library/formatter.cpp
similarity index 100%
rename from src/exprlib/formatter.cpp
rename to src/library/formatter.cpp
diff --git a/src/exprlib/formatter.h b/src/library/formatter.h
similarity index 100%
rename from src/exprlib/formatter.h
rename to src/library/formatter.h
diff --git a/src/exprlib/max_sharing.cpp b/src/library/max_sharing.cpp
similarity index 100%
rename from src/exprlib/max_sharing.cpp
rename to src/library/max_sharing.cpp
diff --git a/src/exprlib/max_sharing.h b/src/library/max_sharing.h
similarity index 100%
rename from src/exprlib/max_sharing.h
rename to src/library/max_sharing.h
diff --git a/src/exprlib/printer.cpp b/src/library/printer.cpp
similarity index 100%
rename from src/exprlib/printer.cpp
rename to src/library/printer.cpp
diff --git a/src/exprlib/printer.h b/src/library/printer.h
similarity index 100%
rename from src/exprlib/printer.h
rename to src/library/printer.h
diff --git a/src/exprlib/state.cpp b/src/library/state.cpp
similarity index 100%
rename from src/exprlib/state.cpp
rename to src/library/state.cpp
diff --git a/src/exprlib/state.h b/src/library/state.h
similarity index 100%
rename from src/exprlib/state.h
rename to src/library/state.h
diff --git a/src/exprlib/toplevel.cpp b/src/library/toplevel.cpp
similarity index 100%
rename from src/exprlib/toplevel.cpp
rename to src/library/toplevel.cpp
diff --git a/src/exprlib/toplevel.h b/src/library/toplevel.h
similarity index 100%
rename from src/exprlib/toplevel.h
rename to src/library/toplevel.h