diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index e7a6a85413..1e8273147d 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -8,11 +8,11 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
 #include "kernel/type_checker.h"
+#include "library/util.h"
 #include "frontends/lean/local_decls.h"
+
 namespace lean {
 class parser;
-typedef std::unique_ptr<type_checker> type_checker_ptr;
-
 /** \brief Parse optional '[persistent]' modifier.
     return true if it is was found, and paremeter \c persistent to true.
 */
diff --git a/src/library/util.h b/src/library/util.h
index a6408aed0b..86ebcfc515 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -6,8 +6,11 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
+#include "kernel/type_checker.h"
 
 namespace lean {
+typedef std::unique_ptr<type_checker> type_checker_ptr;
+
 bool has_unit_decls(environment const & env);
 bool has_eq_decls(environment const & env);
 bool has_heq_decls(environment const & env);