diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index b2b9323266..4312fcc9a2 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -760,6 +760,7 @@ public:
     }
 
     expr execute() override {
+        scoped_expr_caching disable(false);
         bool memoize = true;
         bool trusted_only = m_decl.is_trusted();
         type_checker checker(m_env, memoize, trusted_only);