diff --git a/src/builtin/obj/Int.olean b/src/builtin/obj/Int.olean
index a8d2cb76b..0f9ddad3e 100644
Binary files a/src/builtin/obj/Int.olean and b/src/builtin/obj/Int.olean differ
diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean
index 677e5c5a9..16e56518f 100644
Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ
diff --git a/src/builtin/obj/Real.olean b/src/builtin/obj/Real.olean
index eb1548a6c..c095bf86a 100644
Binary files a/src/builtin/obj/Real.olean and b/src/builtin/obj/Real.olean differ
diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean
index d4515e186..9c513c929 100644
Binary files a/src/builtin/obj/cast.olean and b/src/builtin/obj/cast.olean differ
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index ea7dea49c..df1b25d15 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/builtin/obj/specialfn.olean b/src/builtin/obj/specialfn.olean
index 5b301b289..4862612d7 100644
Binary files a/src/builtin/obj/specialfn.olean and b/src/builtin/obj/specialfn.olean differ
diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 379621d20..325e5e200 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -3,6 +3,6 @@ add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   type_checker.cpp builtin.cpp occurs.cpp metavar.cpp
   justification.cpp unification_constraint.cpp kernel_exception.cpp
   type_checker_justification.cpp pos_info_provider.cpp
-  replace_visitor.cpp update_expr.cpp io_state.cpp)
+  replace_visitor.cpp update_expr.cpp io_state.cpp max_sharing.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index d24823c65..b6cb3c80c 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/expr_eq.h"
 #include "kernel/metavar.h"
+#include "kernel/max_sharing.h"
 
 namespace lean {
 static expr g_dummy(mk_var(0));
@@ -345,18 +346,19 @@ static_assert(is_small(expr_kind::Var) && is_small(expr_kind::Constant) && is_sm
 
 class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
     typedef object_serializer<expr, expr_hash_alloc, expr_eqp> super;
-public:
-    void write(optional<expr> const & a) {
+    max_sharing_fn m_max_sharing_fn;
+
+    void write_core(optional<expr> const & a) {
         serializer & s = get_owner();
         if (a) {
             s << true;
-            write(*a);
+            write_core(*a);
         } else {
             s << false;
         }
     }
 
-    void write(expr const & a) {
+    void write_core(expr const & a) {
         auto k = a.kind();
         char kc;
         if (k == expr_kind::App && num_args(a) < g_small_app_num_args) {
@@ -369,27 +371,31 @@ public:
                 if (kc >= static_cast<char>(g_first_app_size_kind)) {
                     // compressed application
                     for (unsigned i = 0; i < num_args(a); i++)
-                        write(arg(a, i));
+                        write_core(arg(a, i));
                     return;
                 }
                 switch (k) {
                 case expr_kind::Var:       s << var_idx(a); break;
-                case expr_kind::Constant:  s << const_name(a); write(const_type(a)); break;
+                case expr_kind::Constant:  s << const_name(a); write_core(const_type(a)); break;
                 case expr_kind::Type:      s << ty_level(a); break;
                 case expr_kind::Value:     to_value(a).write(s); break;
                 case expr_kind::App:
                     s << num_args(a);
                     for (unsigned i = 0; i < num_args(a); i++)
-                        write(arg(a, i));
+                        write_core(arg(a, i));
                     break;
-                case expr_kind::Eq:        write(eq_lhs(a)); write(eq_rhs(a)); break;
+                case expr_kind::Eq:        write_core(eq_lhs(a)); write_core(eq_rhs(a)); break;
                 case expr_kind::Lambda:
-                case expr_kind::Pi:        s << abst_name(a); write(abst_domain(a)); write(abst_body(a)); break;
-                case expr_kind::Let:       s << let_name(a); write(let_type(a)); write(let_value(a)); write(let_body(a)); break;
+                case expr_kind::Pi:        s << abst_name(a); write_core(abst_domain(a)); write_core(abst_body(a)); break;
+                case expr_kind::Let:       s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a)); break;
                 case expr_kind::MetaVar:   s << metavar_name(a) << metavar_lctx(a); break;
                 }
             });
     }
+public:
+    void write(expr const & a) {
+        write_core(m_max_sharing_fn(a));
+    }
 };
 
 class expr_deserializer : public object_deserializer<expr> {
diff --git a/src/library/max_sharing.cpp b/src/kernel/max_sharing.cpp
similarity index 98%
rename from src/library/max_sharing.cpp
rename to src/kernel/max_sharing.cpp
index a09546a9a..0e7f3e74a 100644
--- a/src/library/max_sharing.cpp
+++ b/src/kernel/max_sharing.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <unordered_set>
 #include <functional>
 #include "util/buffer.h"
-#include "library/max_sharing.h"
+#include "kernel/max_sharing.h"
 
 namespace lean {
 /**
diff --git a/src/library/max_sharing.h b/src/kernel/max_sharing.h
similarity index 100%
rename from src/library/max_sharing.h
rename to src/kernel/max_sharing.h
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 15c95b271..629eec3df 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_library(library kernel_bindings.cpp deep_copy.cpp max_sharing.cpp
+add_library(library kernel_bindings.cpp deep_copy.cpp
   context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp
   fo_unify.cpp bin_op.cpp eq_heq.cpp io_state_stream.cpp printer.cpp)
 
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index b3e14504e..6a9d5f7ed 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -14,8 +14,8 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
+#include "kernel/max_sharing.h"
 #include "library/printer.h"
-#include "library/max_sharing.h"
 #include "library/bin_op.h"
 #include "library/arith/arith.h"
 using namespace lean;
diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp
index 749f819c3..208dc4de2 100644
--- a/src/tests/kernel/threads.cpp
+++ b/src/tests/kernel/threads.cpp
@@ -11,8 +11,8 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/abstract.h"
 #include "kernel/normalizer.h"
+#include "kernel/max_sharing.h"
 #include "library/io_state_stream.h"
-#include "library/max_sharing.h"
 #include "library/deep_copy.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/frontend.h"
diff --git a/src/tests/library/max_sharing.cpp b/src/tests/library/max_sharing.cpp
index 3ba0f8762..11fc67302 100644
--- a/src/tests/library/max_sharing.cpp
+++ b/src/tests/library/max_sharing.cpp
@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #include <iostream>
 #include "util/test.h"
 #include "kernel/abstract.h"
+#include "kernel/max_sharing.h"
 #include "library/printer.h"
-#include "library/max_sharing.h"
 using namespace lean;
 
 static void tst1() {