diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 47acb63989..d0fb5a7531 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -23,8 +23,8 @@ Author: Leonardo de Moura
 #include "library/print.h"
 #include "library/class.h"
 #include "library/flycheck.h"
+#include "library/util.h"
 #include "library/definitional/projection.h"
-#include "library/definitional/util.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/calc.h"
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 40780125e5..f1502d2ba9 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -22,12 +22,12 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/reducible.h"
 #include "library/class.h"
+#include "library/util.h"
 #include "library/definitional/rec_on.h"
 #include "library/definitional/induction_on.h"
 #include "library/definitional/cases_on.h"
 #include "library/definitional/brec_on.h"
 #include "library/definitional/no_confusion.h"
-#include "library/definitional/util.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 1278a7d87a..34a6a582d6 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -27,10 +27,10 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/protected.h"
 #include "library/class.h"
+#include "library/util.h"
 #include "library/definitional/rec_on.h"
 #include "library/definitional/induction_on.h"
 #include "library/definitional/cases_on.h"
-#include "library/definitional/util.h"
 #include "library/definitional/projection.h"
 #include "library/definitional/no_confusion.h"
 #include "frontends/lean/parser.h"
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 084548a239..40a67c1786 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -7,7 +7,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   standard_kernel.cpp sorry.cpp replace_visitor.cpp
   unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
   explicit.cpp num.cpp string.cpp head_map.cpp match.cpp
-  definition_cache.cpp declaration_index.cpp class.cpp
+  definition_cache.cpp declaration_index.cpp class.cpp util.cpp
   print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp
   protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp
   fingerprint.cpp flycheck.cpp hott_kernel.cpp)
diff --git a/src/library/definitional/CMakeLists.txt b/src/library/definitional/CMakeLists.txt
index 512f0886fd..569c27c5ce 100644
--- a/src/library/definitional/CMakeLists.txt
+++ b/src/library/definitional/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp
-  no_confusion.cpp util.cpp projection.cpp brec_on.cpp equations.cpp
+  no_confusion.cpp projection.cpp brec_on.cpp equations.cpp
   init_module.cpp)
 
 target_link_libraries(definitional ${LEAN_LIBS})
diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp
index 9c1352a364..c4b50602b8 100644
--- a/src/library/definitional/brec_on.cpp
+++ b/src/library/definitional/brec_on.cpp
@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/module.h"
 #include "library/bin_app.h"
-#include "library/definitional/util.h"
+#include "library/util.h"
 
 namespace lean {
 static void throw_corrupted(name const & n) {
diff --git a/src/library/definitional/induction_on.cpp b/src/library/definitional/induction_on.cpp
index cfc5b23c6d..b1c7c499a2 100644
--- a/src/library/definitional/induction_on.cpp
+++ b/src/library/definitional/induction_on.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/module.h"
 #include "library/protected.h"
-#include "library/definitional/util.h"
+#include "library/util.h"
 
 namespace lean {
 environment mk_induction_on(environment const & env, name const & n) {
diff --git a/src/library/definitional/init_module.cpp b/src/library/definitional/init_module.cpp
index 89ab0bd352..fd527cbad1 100644
--- a/src/library/definitional/init_module.cpp
+++ b/src/library/definitional/init_module.cpp
@@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/definitional/util.h"
+#include "library/util.h"
 #include "library/definitional/equations.h"
 
 namespace lean{
 void initialize_definitional_module() {
-    initialize_definitional_util();
     initialize_equations();
 }
 
 void finalize_definitional_module() {
     finalize_equations();
-    finalize_definitional_util();
 }
 }
diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp
index d364644575..c01c487748 100644
--- a/src/library/definitional/no_confusion.cpp
+++ b/src/library/definitional/no_confusion.cpp
@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/protected.h"
 #include "library/module.h"
-#include "library/definitional/util.h"
+#include "library/util.h"
 
 namespace lean {
 static void throw_corrupted(name const & n) {
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 00dedd85ec..0b5c9da502 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/placeholder.h"
 #include "library/print.h"
 #include "library/fingerprint.h"
+#include "library/util.h"
 
 namespace lean {
 void initialize_library_module() {
@@ -59,9 +60,11 @@ void initialize_library_module() {
     initialize_unifier_plugin();
     initialize_sorry();
     initialize_class();
+    initialize_library_util();
 }
 
 void finalize_library_module() {
+    finalize_library_util();
     finalize_class();
     finalize_sorry();
     finalize_unifier_plugin();
diff --git a/src/library/definitional/util.cpp b/src/library/util.cpp
similarity index 99%
rename from src/library/definitional/util.cpp
rename to src/library/util.cpp
index cfe8bcb688..afb3880c31 100644
--- a/src/library/definitional/util.cpp
+++ b/src/library/util.cpp
@@ -155,7 +155,7 @@ static name * g_eq_name = nullptr;
 static name * g_eq_refl_name = nullptr;
 static name * g_eq_rec_name = nullptr;
 
-void initialize_definitional_util() {
+void initialize_library_util() {
     g_true           = new expr(mk_constant("true"));
     g_true_intro     = new expr(mk_constant(name({"true", "intro"})));
     g_and            = new expr(mk_constant("and"));
@@ -175,7 +175,7 @@ void initialize_definitional_util() {
     g_eq_rec_name    = new name{"eq", "rec"};
 }
 
-void finalize_definitional_util() {
+void finalize_library_util() {
     delete g_true;
     delete g_true_intro;
     delete g_and;
diff --git a/src/library/definitional/util.h b/src/library/util.h
similarity index 98%
rename from src/library/definitional/util.h
rename to src/library/util.h
index cd02647af5..b3a91814a5 100644
--- a/src/library/definitional/util.h
+++ b/src/library/util.h
@@ -86,6 +86,6 @@ void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> &
 
 level mk_max(levels const & ls);
 
-void initialize_definitional_util();
-void finalize_definitional_util();
+void initialize_library_util();
+void finalize_library_util();
 }