diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt
index 69c60bc7d..8ab41f155 100644
--- a/src/tactic/core/CMakeLists.txt
+++ b/src/tactic/core/CMakeLists.txt
@@ -6,7 +6,6 @@ z3_add_component(core_tactics
     ctx_simplify_tactic.cpp
     elim_term_ite_tactic.cpp
     elim_uncnstr_tactic.cpp
-    injectivity_tactic.cpp
     nnf_tactic.cpp
     occf_tactic.cpp
     pb_preprocess_tactic.cpp
diff --git a/src/tactic/core/injectivity_tactic.h b/src/tactic/core/injectivity_tactic.h
index d0bdfa283..06a841fe6 100644
--- a/src/tactic/core/injectivity_tactic.h
+++ b/src/tactic/core/injectivity_tactic.h
@@ -50,9 +50,7 @@ Tactic Documentation:
 class ast_manager;
 class tactic;
 
-tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p = params_ref());
-
-inline tactic* mk_injectivity2_tactic(ast_manager& m, params_ref const& p = params_ref()) {
+inline tactic* mk_injectivity_tactic(ast_manager& m, params_ref const& p = params_ref()) {
     return alloc(dependent_expr_state_tactic, m, p,
         [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
             return alloc(injectivity_simplifier, m, p, s);
@@ -61,7 +59,6 @@ inline tactic* mk_injectivity2_tactic(ast_manager& m, params_ref const& p = para
 
 /*
   ADD_TACTIC("injectivity",  "Identifies and applies injectivity axioms.", "mk_injectivity_tactic(m, p)")
-  ADD_TACTIC("injectivity2", "Identifies and applies injectivity axioms.", "mk_injectivity2_tactic(m, p)")
   ADD_SIMPLIFIER("injectivity", "Identifies and applies injectivity axioms.", "alloc(injectivity_simplifier, m, p, s)")
 */