diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 1ff4d103a..72feda658 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -1472,7 +1472,7 @@ static environment abstract_expr_cmd(parser & p) {
     app_builder builder(p.env(), p.ios());
     fun_info_manager fun_info(ctx);
     congr_lemma_manager congr_lemma(builder, fun_info);
-    abstract_expr_manager ae_manager(fun_info, congr_lemma);
+    abstract_expr_manager ae_manager(congr_lemma);
 
     flycheck_information info(p.regular_stream());
     if (info.enabled()) p.display_information_pos(p.cmd_pos());
diff --git a/src/library/abstract_expr_manager.cpp b/src/library/abstract_expr_manager.cpp
index ac33482a7..8d93a0a12 100644
--- a/src/library/abstract_expr_manager.cpp
+++ b/src/library/abstract_expr_manager.cpp
@@ -24,18 +24,16 @@ unsigned abstract_expr_manager::hash(expr const & e) {
     case expr_kind::App:
         buffer<expr> args;
         expr f = get_app_args(e, args);
-        fun_info f_info = m_fun_info_manager.get(f, args.size());
         optional<congr_lemma> f_congr = m_congr_lemma_manager.mk_congr(f, args.size());
         unsigned h = hash(f);
         if (!f_congr) {
             for (expr const & arg : args) h = ::lean::hash(h, hash(arg));
         } else {
             int i = -1;
-            for_each2(f_info.get_params_info(), f_congr->get_arg_kinds(),
-                      [&](param_info const & p_info, congr_arg_kind const & c_kind) {
-                          i++;
-                          if (p_info.is_subsingleton() && c_kind == congr_arg_kind::Cast) return;
-                          h = ::lean::hash(h, hash(args[i]));
+            for_each(f_congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) {
+                    i++;
+                    if (c_kind == congr_arg_kind::Cast) return;
+                    h = ::lean::hash(h, hash(args[i]));
                 });
         }
         return h;
@@ -71,7 +69,6 @@ bool abstract_expr_manager::is_equal(expr const & a, expr const & b) {
             expr f_b = get_app_args(b, b_args);
             if (!is_equal(f_a, f_b)) return false;
             if (a_args.size() != b_args.size()) return false;
-            fun_info f_info = m_fun_info_manager.get(f_a, a_args.size());
             optional<congr_lemma> f_congr = m_congr_lemma_manager.mk_congr(f_a, a_args.size());
             bool not_equal = false;
             if (!f_congr) {
@@ -83,13 +80,12 @@ bool abstract_expr_manager::is_equal(expr const & a, expr const & b) {
                 }
             } else {
                 int i = -1;
-                for_each2(f_info.get_params_info(), f_congr->get_arg_kinds(),
-                          [&](param_info const & p_info, congr_arg_kind const & c_kind) {
-                              if (not_equal) return;
-                              i++;
-                              if (p_info.is_subsingleton() && c_kind == congr_arg_kind::Cast) return;
-                              if (!is_equal(a_args[i], b_args[i])) not_equal = true;
-                          });
+                for_each(f_congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) {
+                        if (not_equal) return;
+                        i++;
+                        if (c_kind == congr_arg_kind::Cast) return;
+                        if (!is_equal(a_args[i], b_args[i])) not_equal = true;
+                    });
             }
             return !not_equal;
         }
diff --git a/src/library/abstract_expr_manager.h b/src/library/abstract_expr_manager.h
index 9e1fa86bc..8d26d06a1 100644
--- a/src/library/abstract_expr_manager.h
+++ b/src/library/abstract_expr_manager.h
@@ -13,11 +13,9 @@ namespace lean {
 /** \brief Abstract expression manager, to allow comparing expressions while ignoring subsingletons. */
 
 class abstract_expr_manager {
-    fun_info_manager    & m_fun_info_manager;
     congr_lemma_manager & m_congr_lemma_manager;
 public:
-    abstract_expr_manager(fun_info_manager & f_info_manager, congr_lemma_manager & c_lemma_manager):
-        m_fun_info_manager(f_info_manager), m_congr_lemma_manager(c_lemma_manager) { }
+    abstract_expr_manager(congr_lemma_manager & c_lemma_manager): m_congr_lemma_manager(c_lemma_manager) {}
     unsigned hash(expr const & e);
     bool is_equal(expr const & a, expr const & b);
 };
diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index 335bfe8c6..e35a9b5e2 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -475,7 +475,7 @@ public:
         m_app_builder(*m_tmp_ctx),
         m_fun_info_manager(*m_tmp_ctx),
         m_congr_lemma_manager(m_app_builder, m_fun_info_manager),
-        m_abstract_expr_manager(m_fun_info_manager, m_congr_lemma_manager),
+        m_abstract_expr_manager(m_congr_lemma_manager),
         m_light_lt_manager(env),
         m_rel_getter(mk_relation_info_getter(env)),
         m_refl_getter(mk_refl_info_getter(env)),