diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index aab155a8a..d9e99e761 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -18,21 +18,51 @@ namespace lean {
 */
 struct max_sharing_fn::imp {
     typedef typename std::unordered_set<expr, expr_hash, is_bi_equal_proc> expr_cache;
+    typedef typename std::unordered_set<level, level_hash>                 level_cache;
+    expr_cache  m_expr_cache;
+    level_cache m_lvl_cache;
 
-    expr_cache m_cache;
+    level apply(level const & l) {
+        auto r = m_lvl_cache.find(l);
+        if (r != m_lvl_cache.end())
+            return *r;
+        level res;
+        switch (l.kind()) {
+        case level_kind::Zero:   case level_kind::Param:
+        case level_kind::Global: case level_kind::Meta:
+            res = l;
+            break;
+        case level_kind::Succ:
+            res = update_succ(l, apply(succ_of(l)));
+            break;
+        case level_kind::Max:
+            res = update_max(l, apply(max_lhs(l)), apply(max_rhs(l)));
+            break;
+        case level_kind::IMax:
+            res = update_max(l, apply(imax_lhs(l)), apply(imax_rhs(l)));
+            break;
+        }
+        m_lvl_cache.insert(res);
+        return res;
+    }
 
     expr apply(expr const & a) {
         check_system("max_sharing");
-        auto r = m_cache.find(a);
-        if (r != m_cache.end())
+        auto r = m_expr_cache.find(a);
+        if (r != m_expr_cache.end())
             return *r;
         expr res;
         switch (a.kind()) {
-        case expr_kind::Constant: case expr_kind::Var:
-        case expr_kind::Sort:
+        case expr_kind::Var:
             res = a;
             break;
-          case expr_kind::App:
+        case expr_kind::Constant:
+            res = update_constant(a, map(const_levels(a), [&](level const & l) { return apply(l); }));
+            break;
+        case expr_kind::Sort:
+            res = update_sort(a, apply(sort_level(a)));
+            break;
+        case expr_kind::App:
             res = update_app(a, apply(app_fn(a)), apply(app_arg(a)));
             break;
         case expr_kind::Lambda: case expr_kind::Pi:
@@ -48,7 +78,7 @@ struct max_sharing_fn::imp {
             res = update_macro(a, new_args.size(), new_args.data());
             break;
         }}
-        m_cache.insert(res);
+        m_expr_cache.insert(res);
         return res;
     }
 
@@ -59,15 +89,15 @@ struct max_sharing_fn::imp {
     }
 
     bool already_processed(expr const & a) const {
-        auto r = m_cache.find(a);
-        return r != m_cache.end() && is_eqp(*r, a);
+        auto r = m_expr_cache.find(a);
+        return r != m_expr_cache.end() && is_eqp(*r, a);
     }
 };
 
 max_sharing_fn::max_sharing_fn():m_ptr(new imp) {}
 max_sharing_fn::~max_sharing_fn() {}
 expr max_sharing_fn::operator()(expr const & a) { return (*m_ptr)(a); }
-void max_sharing_fn::clear() { m_ptr->m_cache.clear(); }
+void max_sharing_fn::clear() { m_ptr->m_expr_cache.clear(); }
 bool max_sharing_fn::already_processed(expr const & a) const { return m_ptr->already_processed(a); }
 
 expr max_sharing(expr const & a) {