diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp
index ef080472a4..03b0aa2777 100644
--- a/src/kernel/quot.cpp
+++ b/src/kernel/quot.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 Quotient types.
 */
 #include "util/name_generator.h"
-#include "kernel/old_type_checker.h"
 #include "kernel/quot.h"
 #include "kernel/local_ctx.h"
 #include "kernel/inductive/inductive.h"