diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4e1904093..8f3c296fd 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -52,7 +52,6 @@ endif()
 
 include_directories(${LEAN_SOURCE_DIR}/util)
 include_directories(${LEAN_SOURCE_DIR}/util/numerics)
-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)
@@ -62,8 +61,6 @@ add_subdirectory(util)
 set(EXTRA_LIBS ${EXTRA_LIBS} util)
 add_subdirectory(util/numerics)
 set(EXTRA_LIBS ${EXTRA_LIBS} numerics)
-add_subdirectory(util/sexpr)
-set(EXTRA_LIBS ${EXTRA_LIBS} sexpr)
 add_subdirectory(interval)
 set(EXTRA_LIBS ${EXTRA_LIBS} interval)
 add_subdirectory(kernel)
@@ -76,6 +73,5 @@ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
 add_subdirectory(shell)
 add_subdirectory(tests/util)
 add_subdirectory(tests/util/numerics)
-add_subdirectory(tests/util/sexpr)
 add_subdirectory(tests/interval)
 add_subdirectory(tests/kernel)
diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index 5d973fdcf..7317560b8 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -4,6 +4,9 @@ add_test(interrupt ${CMAKE_CURRENT_BINARY_DIR}/interrupt)
 add_executable(name name.cpp)
 target_link_libraries(name ${EXTRA_LIBS})
 add_test(name ${CMAKE_CURRENT_BINARY_DIR}/name)
+add_executable(sexpr sexpr.cpp)
+target_link_libraries(sexpr ${EXTRA_LIBS})
+add_test(sexpr ${CMAKE_CURRENT_BINARY_DIR}/sexpr)
 add_executable(format format.cpp)
 target_link_libraries(format ${EXTRA_LIBS})
 add_test(format ${CMAKE_CURRENT_BINARY_DIR}/format)
diff --git a/src/tests/util/sexpr/sexpr.cpp b/src/tests/util/sexpr.cpp
similarity index 100%
rename from src/tests/util/sexpr/sexpr.cpp
rename to src/tests/util/sexpr.cpp
diff --git a/src/tests/util/sexpr/CMakeLists.txt b/src/tests/util/sexpr/CMakeLists.txt
deleted file mode 100644
index 686bcd03d..000000000
--- a/src/tests/util/sexpr/CMakeLists.txt
+++ /dev/null
@@ -1,3 +0,0 @@
-add_executable(sexpr_tst sexpr.cpp)
-target_link_libraries(sexpr_tst ${EXTRA_LIBS})
-add_test(sexpr ${CMAKE_CURRENT_BINARY_DIR}/sexpr_tst)
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 43a19f2e9..3fc0f47a7 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(util trace.cpp debug.cpp name.cpp exception.cpp
   verbosity.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp
-  format.cpp safe_arith.cpp options.cpp
+  sexpr.cpp sexpr_funcs.cpp format.cpp safe_arith.cpp options.cpp
   )
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr.cpp
similarity index 100%
rename from src/util/sexpr/sexpr.cpp
rename to src/util/sexpr.cpp
diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr.h
similarity index 98%
rename from src/util/sexpr/sexpr.h
rename to src/util/sexpr.h
index b1e0d1471..702cbdb04 100644
--- a/src/util/sexpr/sexpr.h
+++ b/src/util/sexpr.h
@@ -136,6 +136,7 @@ inline bool operator==(sexpr const & a, bool b) { return is_int(a) && to_bool(a)
 inline bool operator==(sexpr const & a, int b) { return is_int(a) && to_int(a) == b; }
 inline bool operator==(sexpr const & a, double b) { return is_double(a) && to_double(a) == b; }
 inline bool operator==(sexpr const & a, std::string const & b) { return is_string(a) && to_string(a) == b; }
+inline bool operator==(sexpr const & a, char const * b) { return is_string(a) && to_string(a) == b; }
 bool operator==(sexpr const & a, name const & b);
 bool operator==(sexpr const & a, mpz const & b);
 bool operator==(sexpr const & a, mpq const & b);
diff --git a/src/util/sexpr/CMakeLists.txt b/src/util/sexpr/CMakeLists.txt
deleted file mode 100644
index 7a965ada1..000000000
--- a/src/util/sexpr/CMakeLists.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-add_library(sexpr sexpr.cpp sexpr_funcs.cpp)
-target_link_libraries(sexpr ${EXTRA_LIBS})
diff --git a/src/util/sexpr/sexpr_funcs.cpp b/src/util/sexpr_funcs.cpp
similarity index 100%
rename from src/util/sexpr/sexpr_funcs.cpp
rename to src/util/sexpr_funcs.cpp
diff --git a/src/util/sexpr/sexpr_funcs.h b/src/util/sexpr_funcs.h
similarity index 100%
rename from src/util/sexpr/sexpr_funcs.h
rename to src/util/sexpr_funcs.h