diff --git a/src/library/abstract_context_cache.h b/src/library/abstract_context_cache.h
index 4bf1570991..479ccd9241 100644
--- a/src/library/abstract_context_cache.h
+++ b/src/library/abstract_context_cache.h
@@ -213,48 +213,48 @@ public:
 
     /* Cache support for fun_info module */
 
-    virtual optional<fun_info> get_fun_info(type_context_old &, expr const &) = 0;
-    virtual void set_fun_info(type_context_old &, expr const &, fun_info const &) = 0;
+    virtual optional<fun_info> get_fun_info(expr const &) = 0;
+    virtual void set_fun_info(expr const &, fun_info const &) = 0;
 
-    virtual optional<fun_info> get_fun_info_nargs(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_fun_info_nargs(type_context_old &, expr const &, unsigned, fun_info const &) = 0;
+    virtual optional<fun_info> get_fun_info_nargs(expr const &, unsigned) = 0;
+    virtual void set_fun_info_nargs(expr const &, unsigned, fun_info const &) = 0;
 
-    virtual optional<unsigned> get_specialization_prefix_size(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_specialization_prefix_size(type_context_old &, expr const &, unsigned, unsigned) = 0;
+    virtual optional<unsigned> get_specialization_prefix_size(expr const &, unsigned) = 0;
+    virtual void set_specialization_prefix_size(expr const &, unsigned, unsigned) = 0;
 
-    virtual optional<ss_param_infos> get_subsingleton_info(type_context_old &, expr const &) = 0;
-    virtual void set_subsingleton_info(type_context_old &, expr const &, ss_param_infos const &) = 0;
+    virtual optional<ss_param_infos> get_subsingleton_info(expr const &) = 0;
+    virtual void set_subsingleton_info(expr const &, ss_param_infos const &) = 0;
 
-    virtual optional<ss_param_infos> get_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) = 0;
+    virtual optional<ss_param_infos> get_subsingleton_info_nargs(expr const &, unsigned) = 0;
+    virtual void set_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) = 0;
 
-    virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_specialization_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) = 0;
+    virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(expr const &, unsigned) = 0;
+    virtual void set_specialization_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) = 0;
 
     /* Cache support for congr_lemma module */
 
-    virtual optional<congr_lemma> get_simp_congr_lemma(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
+    virtual optional<congr_lemma> get_simp_congr_lemma(expr const &, unsigned) = 0;
+    virtual void set_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
 
-    virtual optional<congr_lemma> get_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
+    virtual optional<congr_lemma> get_specialized_simp_congr_lemma(expr const &, unsigned) = 0;
+    virtual void set_specialized_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
 
-    virtual optional<congr_lemma> get_congr_lemma(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
+    virtual optional<congr_lemma> get_congr_lemma(expr const &, unsigned) = 0;
+    virtual void set_congr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
 
-    virtual optional<congr_lemma> get_specialized_congr_lemma(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_specialized_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
+    virtual optional<congr_lemma> get_specialized_congr_lemma(expr const &, unsigned) = 0;
+    virtual void set_specialized_congr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
 
-    virtual optional<congr_lemma> get_hcongr_lemma(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_hcongr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
+    virtual optional<congr_lemma> get_hcongr_lemma(expr const &, unsigned) = 0;
+    virtual void set_hcongr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
 
     /* Cache support for app_builder */
 
-    virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, unsigned) = 0;
-    virtual void set_app_builder_info(type_context_old &, expr const &, unsigned, app_builder_info const &) = 0;
+    virtual optional<app_builder_info> get_app_builder_info(expr const &, unsigned) = 0;
+    virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) = 0;
 
-    virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, list<bool> const &) = 0;
-    virtual void set_app_builder_info(type_context_old &, expr const &, list<bool> const &, app_builder_info const &) = 0;
+    virtual optional<app_builder_info> get_app_builder_info(expr const &, list<bool> const &) = 0;
+    virtual void set_app_builder_info(expr const &, list<bool> const &, app_builder_info const &) = 0;
 };
 
 /* Dummy implementation of the abstract_context_cache interface that does not do cache anything but configuration options. */
@@ -324,48 +324,48 @@ public:
 
     /* Cache support for fun_info module */
 
-    virtual optional<fun_info> get_fun_info(type_context_old &, expr const &) override { return optional<fun_info>(); }
-    virtual void set_fun_info(type_context_old &, expr const &, fun_info const &) override {}
+    virtual optional<fun_info> get_fun_info(expr const &) override { return optional<fun_info>(); }
+    virtual void set_fun_info(expr const &, fun_info const &) override {}
 
-    virtual optional<fun_info> get_fun_info_nargs(type_context_old &, expr const &, unsigned) override { return optional<fun_info>(); }
-    virtual void set_fun_info_nargs(type_context_old &, expr const &, unsigned, fun_info const &) override {}
+    virtual optional<fun_info> get_fun_info_nargs(expr const &, unsigned) override { return optional<fun_info>(); }
+    virtual void set_fun_info_nargs(expr const &, unsigned, fun_info const &) override {}
 
-    virtual optional<unsigned> get_specialization_prefix_size(type_context_old &, expr const &, unsigned) override { return optional<unsigned>(); }
-    virtual void set_specialization_prefix_size(type_context_old &, expr const &, unsigned, unsigned) override {}
+    virtual optional<unsigned> get_specialization_prefix_size(expr const &, unsigned) override { return optional<unsigned>(); }
+    virtual void set_specialization_prefix_size(expr const &, unsigned, unsigned) override {}
 
-    virtual optional<ss_param_infos> get_subsingleton_info(type_context_old &, expr const &) override { return optional<ss_param_infos>(); }
-    virtual void set_subsingleton_info(type_context_old &, expr const &, ss_param_infos const &) override {}
+    virtual optional<ss_param_infos> get_subsingleton_info(expr const &) override { return optional<ss_param_infos>(); }
+    virtual void set_subsingleton_info(expr const &, ss_param_infos const &) override {}
 
-    virtual optional<ss_param_infos> get_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) override { return optional<ss_param_infos>(); }
-    virtual void set_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) override {}
+    virtual optional<ss_param_infos> get_subsingleton_info_nargs(expr const &, unsigned) override { return optional<ss_param_infos>(); }
+    virtual void set_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) override {}
 
-    virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) override { return optional<ss_param_infos>(); }
-    virtual void set_specialization_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) override {}
+    virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(expr const &, unsigned) override { return optional<ss_param_infos>(); }
+    virtual void set_specialization_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) override {}
 
     /* Cache support for congr_lemma module */
 
-    virtual optional<congr_lemma> get_simp_congr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
-    virtual void set_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
+    virtual optional<congr_lemma> get_simp_congr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
+    virtual void set_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) override {}
 
-    virtual optional<congr_lemma> get_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
-    virtual void set_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
+    virtual optional<congr_lemma> get_specialized_simp_congr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
+    virtual void set_specialized_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) override {}
 
-    virtual optional<congr_lemma> get_congr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
-    virtual void set_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
+    virtual optional<congr_lemma> get_congr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
+    virtual void set_congr_lemma(expr const &, unsigned, congr_lemma const &) override {}
 
-    virtual optional<congr_lemma> get_specialized_congr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
-    virtual void set_specialized_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
+    virtual optional<congr_lemma> get_specialized_congr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
+    virtual void set_specialized_congr_lemma(expr const &, unsigned, congr_lemma const &) override {}
 
-    virtual optional<congr_lemma> get_hcongr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
-    virtual void set_hcongr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
+    virtual optional<congr_lemma> get_hcongr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
+    virtual void set_hcongr_lemma(expr const &, unsigned, congr_lemma const &) override {}
 
     /* Cache support for app_builder */
 
-    virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, unsigned) override { return optional<app_builder_info>(); }
-    virtual void set_app_builder_info(type_context_old &, expr const &, unsigned, app_builder_info const &) override {}
+    virtual optional<app_builder_info> get_app_builder_info(expr const &, unsigned) override { return optional<app_builder_info>(); }
+    virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) override {}
 
-    virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, list<bool> const &) override { return optional<app_builder_info>(); }
-    virtual void set_app_builder_info(type_context_old &, expr const &, list<bool> const &, app_builder_info const &) override {}
+    virtual optional<app_builder_info> get_app_builder_info(expr const &, list<bool> const &) override { return optional<app_builder_info>(); }
+    virtual void set_app_builder_info(expr const &, list<bool> const &, app_builder_info const &) override {}
 };
 
 void initialize_abstract_context_cache();
diff --git a/src/library/persistent_context_cache.cpp b/src/library/persistent_context_cache.cpp
index 255db2ace9..6ecaf6f084 100644
--- a/src/library/persistent_context_cache.cpp
+++ b/src/library/persistent_context_cache.cpp
@@ -131,109 +131,109 @@ optional<local_instances> persistent_context_cache::get_frozen_local_instances()
     return m_cache_ptr->get_frozen_local_instances();
 }
 
-optional<fun_info> persistent_context_cache::get_fun_info(type_context_old & ctx, expr const & e) {
-    return m_cache_ptr->get_fun_info(ctx, e);
+optional<fun_info> persistent_context_cache::get_fun_info(expr const & e) {
+    return m_cache_ptr->get_fun_info(e);
 }
 
-void persistent_context_cache::set_fun_info(type_context_old & ctx, expr const & e, fun_info const & r) {
-    return m_cache_ptr->set_fun_info(ctx, e, r);
+void persistent_context_cache::set_fun_info(expr const & e, fun_info const & r) {
+    return m_cache_ptr->set_fun_info(e, r);
 }
 
-optional<fun_info> persistent_context_cache::get_fun_info_nargs(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_fun_info_nargs(ctx, e, k);
+optional<fun_info> persistent_context_cache::get_fun_info_nargs(expr const & e, unsigned k) {
+    return m_cache_ptr->get_fun_info_nargs(e, k);
 }
 
-void persistent_context_cache::set_fun_info_nargs(type_context_old & ctx, expr const & e, unsigned k, fun_info const & r) {
-    return m_cache_ptr->set_fun_info_nargs(ctx, e, k, r);
+void persistent_context_cache::set_fun_info_nargs(expr const & e, unsigned k, fun_info const & r) {
+    return m_cache_ptr->set_fun_info_nargs(e, k, r);
 }
 
-optional<unsigned> persistent_context_cache::get_specialization_prefix_size(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_specialization_prefix_size(ctx, e, k);
+optional<unsigned> persistent_context_cache::get_specialization_prefix_size(expr const & e, unsigned k) {
+    return m_cache_ptr->get_specialization_prefix_size(e, k);
 }
 
-void persistent_context_cache::set_specialization_prefix_size(type_context_old & ctx, expr const & e, unsigned k, unsigned r) {
-    return m_cache_ptr->set_specialization_prefix_size(ctx, e, k, r);
+void persistent_context_cache::set_specialization_prefix_size(expr const & e, unsigned k, unsigned r) {
+    return m_cache_ptr->set_specialization_prefix_size(e, k, r);
 }
 
-optional<ss_param_infos> persistent_context_cache::get_subsingleton_info(type_context_old & ctx, expr const & e) {
-    return m_cache_ptr->get_subsingleton_info(ctx, e);
+optional<ss_param_infos> persistent_context_cache::get_subsingleton_info(expr const & e) {
+    return m_cache_ptr->get_subsingleton_info(e);
 }
 
-void persistent_context_cache::set_subsingleton_info(type_context_old & ctx, expr const & e, ss_param_infos const & r) {
-    return m_cache_ptr->set_subsingleton_info(ctx, e, r);
+void persistent_context_cache::set_subsingleton_info(expr const & e, ss_param_infos const & r) {
+    return m_cache_ptr->set_subsingleton_info(e, r);
 }
 
-optional<ss_param_infos> persistent_context_cache::get_subsingleton_info_nargs(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_subsingleton_info_nargs(ctx, e, k);
+optional<ss_param_infos> persistent_context_cache::get_subsingleton_info_nargs(expr const & e, unsigned k) {
+    return m_cache_ptr->get_subsingleton_info_nargs(e, k);
 }
 
-void persistent_context_cache::set_subsingleton_info_nargs(type_context_old & ctx, expr const & e, unsigned k, ss_param_infos const & r) {
-    return m_cache_ptr->set_subsingleton_info_nargs(ctx, e, k, r);
+void persistent_context_cache::set_subsingleton_info_nargs(expr const & e, unsigned k, ss_param_infos const & r) {
+    return m_cache_ptr->set_subsingleton_info_nargs(e, k, r);
 }
 
-optional<ss_param_infos> persistent_context_cache::get_specialized_subsingleton_info_nargs(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_specialized_subsingleton_info_nargs(ctx, e, k);
+optional<ss_param_infos> persistent_context_cache::get_specialized_subsingleton_info_nargs(expr const & e, unsigned k) {
+    return m_cache_ptr->get_specialized_subsingleton_info_nargs(e, k);
 }
 
-void persistent_context_cache::set_specialization_subsingleton_info_nargs(type_context_old & ctx, expr const & e, unsigned k, ss_param_infos const & r) {
-    return m_cache_ptr->set_specialization_subsingleton_info_nargs(ctx, e, k, r);
+void persistent_context_cache::set_specialization_subsingleton_info_nargs(expr const & e, unsigned k, ss_param_infos const & r) {
+    return m_cache_ptr->set_specialization_subsingleton_info_nargs(e, k, r);
 }
 
-optional<congr_lemma> persistent_context_cache::get_simp_congr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_simp_congr_lemma(ctx, e, k);
+optional<congr_lemma> persistent_context_cache::get_simp_congr_lemma(expr const & e, unsigned k) {
+    return m_cache_ptr->get_simp_congr_lemma(e, k);
 }
 
-void persistent_context_cache::set_simp_congr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
-    return m_cache_ptr->set_simp_congr_lemma(ctx, e, k, r);
+void persistent_context_cache::set_simp_congr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
+    return m_cache_ptr->set_simp_congr_lemma(e, k, r);
 }
 
-optional<congr_lemma> persistent_context_cache::get_specialized_simp_congr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_specialized_simp_congr_lemma(ctx, e, k);
+optional<congr_lemma> persistent_context_cache::get_specialized_simp_congr_lemma(expr const & e, unsigned k) {
+    return m_cache_ptr->get_specialized_simp_congr_lemma(e, k);
 }
 
-void persistent_context_cache::set_specialized_simp_congr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
-    return m_cache_ptr->set_specialized_simp_congr_lemma(ctx, e, k, r);
+void persistent_context_cache::set_specialized_simp_congr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
+    return m_cache_ptr->set_specialized_simp_congr_lemma(e, k, r);
 }
 
-optional<congr_lemma> persistent_context_cache::get_congr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_congr_lemma(ctx, e, k);
+optional<congr_lemma> persistent_context_cache::get_congr_lemma(expr const & e, unsigned k) {
+    return m_cache_ptr->get_congr_lemma(e, k);
 }
 
-void persistent_context_cache::set_congr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
-    return m_cache_ptr->set_congr_lemma(ctx, e, k, r);
+void persistent_context_cache::set_congr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
+    return m_cache_ptr->set_congr_lemma(e, k, r);
 }
 
-optional<congr_lemma> persistent_context_cache::get_specialized_congr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_specialized_congr_lemma(ctx, e, k);
+optional<congr_lemma> persistent_context_cache::get_specialized_congr_lemma(expr const & e, unsigned k) {
+    return m_cache_ptr->get_specialized_congr_lemma(e, k);
 }
 
-void persistent_context_cache::set_specialized_congr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
-    return m_cache_ptr->set_specialized_congr_lemma(ctx, e, k, r);
+void persistent_context_cache::set_specialized_congr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
+    return m_cache_ptr->set_specialized_congr_lemma(e, k, r);
 }
 
-optional<congr_lemma> persistent_context_cache::get_hcongr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_hcongr_lemma(ctx, e, k);
+optional<congr_lemma> persistent_context_cache::get_hcongr_lemma(expr const & e, unsigned k) {
+    return m_cache_ptr->get_hcongr_lemma(e, k);
 }
 
-void persistent_context_cache::set_hcongr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
-    return m_cache_ptr->set_hcongr_lemma(ctx, e, k, r);
+void persistent_context_cache::set_hcongr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
+    return m_cache_ptr->set_hcongr_lemma(e, k, r);
 }
 
-optional<app_builder_info> persistent_context_cache::get_app_builder_info(type_context_old & ctx, expr const & e, unsigned k) {
-    return m_cache_ptr->get_app_builder_info(ctx, e, k);
+optional<app_builder_info> persistent_context_cache::get_app_builder_info(expr const & e, unsigned k) {
+    return m_cache_ptr->get_app_builder_info(e, k);
 }
 
-void persistent_context_cache::set_app_builder_info(type_context_old & ctx, expr const & e, unsigned k, app_builder_info const & r) {
-    return m_cache_ptr->set_app_builder_info(ctx, e, k, r);
+void persistent_context_cache::set_app_builder_info(expr const & e, unsigned k, app_builder_info const & r) {
+    return m_cache_ptr->set_app_builder_info(e, k, r);
 }
 
 
-optional<app_builder_info> persistent_context_cache::get_app_builder_info(type_context_old & ctx, expr const & e, list<bool> const & m) {
-    return m_cache_ptr->get_app_builder_info(ctx, e, m);
+optional<app_builder_info> persistent_context_cache::get_app_builder_info(expr const & e, list<bool> const & m) {
+    return m_cache_ptr->get_app_builder_info(e, m);
 }
 
-void persistent_context_cache::set_app_builder_info(type_context_old & ctx, expr const & e, list<bool> const & m, app_builder_info const & r) {
-    return m_cache_ptr->set_app_builder_info(ctx, e, m, r);
+void persistent_context_cache::set_app_builder_info(expr const & e, list<bool> const & m, app_builder_info const & r) {
+    return m_cache_ptr->set_app_builder_info(e, m, r);
 }
 
 void initialize_persistent_context_cache() {
diff --git a/src/library/persistent_context_cache.h b/src/library/persistent_context_cache.h
index 555c5cf236..43407131d8 100644
--- a/src/library/persistent_context_cache.h
+++ b/src/library/persistent_context_cache.h
@@ -77,47 +77,47 @@ public:
 
     /* Cache support for fun_info module */
 
-    virtual optional<fun_info> get_fun_info(type_context_old &, expr const &) override;
-    virtual void set_fun_info(type_context_old &, expr const &, fun_info const &) override;
+    virtual optional<fun_info> get_fun_info(expr const &) override;
+    virtual void set_fun_info(expr const &, fun_info const &) override;
 
-    virtual optional<fun_info> get_fun_info_nargs(type_context_old &, expr const &, unsigned) override;
-    virtual void set_fun_info_nargs(type_context_old &, expr const &, unsigned, fun_info const &) override;
+    virtual optional<fun_info> get_fun_info_nargs(expr const &, unsigned) override;
+    virtual void set_fun_info_nargs(expr const &, unsigned, fun_info const &) override;
 
-    virtual optional<unsigned> get_specialization_prefix_size(type_context_old &, expr const &, unsigned) override;
-    virtual void set_specialization_prefix_size(type_context_old &, expr const &, unsigned, unsigned) override;
+    virtual optional<unsigned> get_specialization_prefix_size(expr const &, unsigned) override;
+    virtual void set_specialization_prefix_size(expr const &, unsigned, unsigned) override;
 
-    virtual optional<ss_param_infos> get_subsingleton_info(type_context_old &, expr const &) override;
-    virtual void set_subsingleton_info(type_context_old &, expr const &, ss_param_infos const &) override;
+    virtual optional<ss_param_infos> get_subsingleton_info(expr const &) override;
+    virtual void set_subsingleton_info(expr const &, ss_param_infos const &) override;
 
-    virtual optional<ss_param_infos> get_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) override;
-    virtual void set_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) override;
+    virtual optional<ss_param_infos> get_subsingleton_info_nargs(expr const &, unsigned) override;
+    virtual void set_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) override;
 
-    virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) override;
-    virtual void set_specialization_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) override;
+    virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(expr const &, unsigned) override;
+    virtual void set_specialization_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) override;
 
     /* Cache support for congr_lemma module */
 
-    virtual optional<congr_lemma> get_simp_congr_lemma(type_context_old &, expr const &, unsigned) override;
-    virtual void set_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
+    virtual optional<congr_lemma> get_simp_congr_lemma(expr const &, unsigned) override;
+    virtual void set_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) override;
 
-    virtual optional<congr_lemma> get_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned) override;
-    virtual void set_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
+    virtual optional<congr_lemma> get_specialized_simp_congr_lemma(expr const &, unsigned) override;
+    virtual void set_specialized_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) override;
 
-    virtual optional<congr_lemma> get_congr_lemma(type_context_old &, expr const &, unsigned) override;
-    virtual void set_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
+    virtual optional<congr_lemma> get_congr_lemma(expr const &, unsigned) override;
+    virtual void set_congr_lemma(expr const &, unsigned, congr_lemma const &) override;
 
-    virtual optional<congr_lemma> get_specialized_congr_lemma(type_context_old &, expr const &, unsigned) override;
-    virtual void set_specialized_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
+    virtual optional<congr_lemma> get_specialized_congr_lemma(expr const &, unsigned) override;
+    virtual void set_specialized_congr_lemma(expr const &, unsigned, congr_lemma const &) override;
 
-    virtual optional<congr_lemma> get_hcongr_lemma(type_context_old &, expr const &, unsigned) override;
-    virtual void set_hcongr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
+    virtual optional<congr_lemma> get_hcongr_lemma(expr const &, unsigned) override;
+    virtual void set_hcongr_lemma(expr const &, unsigned, congr_lemma const &) override;
 
     /* Cache support for app_builder */
 
-    virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, unsigned) override;
-    virtual void set_app_builder_info(type_context_old &, expr const &, unsigned, app_builder_info const &) override;
+    virtual optional<app_builder_info> get_app_builder_info(expr const &, unsigned) override;
+    virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) override;
 
-    virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, list<bool> const &) override;
-    virtual void set_app_builder_info(type_context_old &, expr const &, list<bool> const &, app_builder_info const &) override;
+    virtual optional<app_builder_info> get_app_builder_info(expr const &, list<bool> const &) override;
+    virtual void set_app_builder_info(expr const &, list<bool> const &, app_builder_info const &) override;
 };
 }