diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index a43b5416ed..4e6812944b 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -1554,7 +1554,6 @@ class add_nested_inductive_decl_fn {
         cfg.m_canonize_proofs    = false;
         cfg.m_use_axioms         = false;
         cfg.m_zeta               = false;
-        cfg.m_use_matcher        = false;
         return cfg;
     }
 
diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h
index da65748f84..2b568d87f5 100644
--- a/src/library/tactic/simplify.h
+++ b/src/library/tactic/simplify.h
@@ -37,9 +37,6 @@ struct simp_config {
     bool                      m_beta;
     bool                      m_eta;
     bool                      m_proj;
-    /* The following option should be removed as soon as we
-       refactor the inductive compiler. */
-    bool                      m_use_matcher{true};
     simp_config();
     simp_config(vm_obj const & o);
 };