diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt
index 3e9784c07..437c48113 100644
--- a/src/builtin/CMakeLists.txt
+++ b/src/builtin/CMakeLists.txt
@@ -31,7 +31,7 @@ function(add_theory_core FILE ARG EXTRA_DEPS)
     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}
     DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${SHELL_DIR}/lean ${EXTRA_DEPS})
-  add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME})
+  add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${EXTRA_DEPS})
   add_dependencies(builtin ${BASENAME}_builtin)
   install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
 endfunction()
@@ -50,35 +50,27 @@ function(copy_olean FILE)
   install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
 endfunction()
 
-function(add_kernel_theory FILE)
+function(add_kernel_theory FILE DEPS)
   if(CMAKE_CROSSCOMPILING)
     copy_olean(${FILE})
   else()
-    add_theory_core(${FILE} "-n" "${CMAKE_CURRENT_BINARY_DIR}/macros.lua")
+    add_theory_core(${FILE} "-n" "${DEPS}")
   endif()
 endfunction()
 
-function(add_theory FILE)
+function(add_theory FILE DEPS)
   if(CMAKE_CROSSCOMPILING)
     copy_olean(${FILE})
   else()
-    add_theory_core(${FILE} "" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
+    add_theory_core(${FILE} "" "${DEPS}")
   endif()
 endfunction()
 
-add_kernel_theory("kernel.lean")
-add_kernel_theory("nat.lean")
-add_dependencies(nat_builtin kernel_builtin)
-add_kernel_theory("int.lean")
-add_dependencies(int_builtin nat_builtin)
-add_kernel_theory("real.lean")
-add_dependencies(real_builtin int_builtin)
-add_kernel_theory("specialfn.lean")
-add_dependencies(specialfn_builtin real_builtin)
-add_theory("cast.lean")
-# TODO(Leo): Remove the following dependencies after cleanup
-add_dependencies(cast_builtin kernel_builtin)
-add_dependencies(cast_builtin nat_builtin)
-add_dependencies(cast_builtin int_builtin)
-add_dependencies(cast_builtin real_builtin)
-add_dependencies(cast_builtin specialfn_builtin)
+add_kernel_theory("kernel.lean"    "${CMAKE_CURRENT_BINARY_DIR}/macros.lua")
+add_kernel_theory("nat.lean"       "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
+add_kernel_theory("int.lean"       "${CMAKE_CURRENT_BINARY_DIR}/nat.olean")
+add_kernel_theory("real.lean"      "${CMAKE_CURRENT_BINARY_DIR}/int.olean")
+
+add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/real.olean")
+add_theory("cast.lean"      "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
+
diff --git a/src/builtin/specialfn.olean b/src/builtin/specialfn.olean
index 4c47160c6..dc8c45c76 100644
Binary files a/src/builtin/specialfn.olean and b/src/builtin/specialfn.olean differ