diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index 8b986ba89..967bb935a 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -223,11 +223,6 @@ tactic eapply_tactic(elaborate_fn const & elab, expr const & e) {
     return apply_tactic_core(elab, e, AddAll, AddSubgoals);
 }
 
-int mk_eassumption_tactic(lua_State * L) { return push_tactic(L, eassumption_tactic()); }
-void open_apply_tactic(lua_State * L) {
-    SET_GLOBAL_FUN(mk_eassumption_tactic, "eassumption_tac");
-}
-
 void initialize_apply_tactic() {
     g_apply_class_instance = new name{"apply", "class_instance"};
     register_bool_option(*g_apply_class_instance, LEAN_DEFAULT_APPLY_CLASS_INSTANCE,
diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h
index ea73d23e9..1c1a4f5d9 100644
--- a/src/library/tactic/apply_tactic.h
+++ b/src/library/tactic/apply_tactic.h
@@ -14,7 +14,6 @@ tactic apply_tactic(elaborate_fn const & fn, expr const & e);
 tactic fapply_tactic(elaborate_fn const & fn, expr const & e);
 tactic eassumption_tactic();
 tactic assumption_tactic();
-void open_apply_tactic(lua_State * L);
 void initialize_apply_tactic();
 void finalize_apply_tactic();
 }
diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h
index 941425549..62f0d50b4 100644
--- a/src/library/tactic/register_module.h
+++ b/src/library/tactic/register_module.h
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_state.h"
 #include "library/tactic/tactic.h"
-#include "library/tactic/apply_tactic.h"
 // #include "library/tactic/simplify_tactic.h"
 
 namespace lean {
@@ -17,7 +16,6 @@ inline void open_tactic_module(lua_State * L) {
     open_goal(L);
     open_proof_state(L);
     open_tactic(L);
-    open_apply_tactic(L);
     // open_simplify_tactic(L);
 }
 inline void register_tactic_module() {