diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt
index 7d63e7446..ff425ecc3 100644
--- a/src/builtin/CMakeLists.txt
+++ b/src/builtin/CMakeLists.txt
@@ -29,7 +29,7 @@ function(add_theory_core FILE ARG EXTRA_DEPS)
   add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
     COMMAND ${SHELL_DIR}/lean ${ARG} -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE}
     COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${SHELL_DIR}/${FNAME}
-    COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FNAME}
+    COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME}
     DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${SHELL_DIR}/lean ${EXTRA_DEPS})
   add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${EXTRA_DEPS})
   add_dependencies(builtin ${BASENAME}_builtin)
@@ -42,9 +42,9 @@ function(copy_olean FILE)
   get_filename_component(BASENAME ${FILE} NAME_WE)
   set(FNAME "${BASENAME}.olean")
   add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
-    COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/${FNAME} ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
-    COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/${FNAME} ${SHELL_DIR}/${FNAME}
-    DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FNAME})
+    COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME} ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}
+    COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME} ${SHELL_DIR}/${FNAME}
+    DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME})
   add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME})
   add_dependencies(builtin ${BASENAME}_builtin)
   install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
diff --git a/src/builtin/cast.olean b/src/builtin/obj/cast.olean
similarity index 100%
rename from src/builtin/cast.olean
rename to src/builtin/obj/cast.olean
diff --git a/src/builtin/int.olean b/src/builtin/obj/int.olean
similarity index 100%
rename from src/builtin/int.olean
rename to src/builtin/obj/int.olean
diff --git a/src/builtin/kernel.olean b/src/builtin/obj/kernel.olean
similarity index 100%
rename from src/builtin/kernel.olean
rename to src/builtin/obj/kernel.olean
diff --git a/src/builtin/nat.olean b/src/builtin/obj/nat.olean
similarity index 100%
rename from src/builtin/nat.olean
rename to src/builtin/obj/nat.olean
diff --git a/src/builtin/real.olean b/src/builtin/obj/real.olean
similarity index 100%
rename from src/builtin/real.olean
rename to src/builtin/obj/real.olean
diff --git a/src/builtin/specialfn.olean b/src/builtin/obj/specialfn.olean
similarity index 100%
rename from src/builtin/specialfn.olean
rename to src/builtin/obj/specialfn.olean