diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 5d8a442f56..09ece1fab4 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -633,8 +633,8 @@ optional<expr> type_context_old::reduce_projection(expr const & e) {
 }
 
 optional<expr> type_context_old::reduce_proj(expr const & /* e */) {
-    // TODO(Leo):
-    lean_unreachable();
+    // TODO(Leo)
+    throw exception("projection reduction is only implemented in the kernel.");
 }
 
 optional<expr> type_context_old::reduce_aux_recursor(expr const & e) {