diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 6850fec27..7846fb6a4 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -7,6 +7,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   standard_kernel.cpp hott_kernel.cpp
   unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
   explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
-  hop_match.cpp)
+  match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/hop_match.cpp b/src/library/match.cpp
similarity index 88%
rename from src/library/hop_match.cpp
rename to src/library/match.cpp
index abdd00b77..0882323bb 100644
--- a/src/library/hop_match.cpp
+++ b/src/library/match.cpp
@@ -8,14 +8,14 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "library/kernel_bindings.h"
 #include "library/locals.h"
-#include "library/hop_match.h"
+#include "library/match.h"
 
 namespace lean {
-class hop_match_fn {
+class match_fn {
     buffer<optional<expr>> &   m_subst;
     name_generator             m_ngen;
     name_map<name> *           m_name_subst;
-    hop_matcher_plugin const * m_plugin;
+    matcher_plugin const * m_plugin;
 
     void assign(expr const & p, expr const & t) {
         lean_assert(var_idx(p) < m_subst.size());
@@ -117,7 +117,7 @@ class hop_match_fn {
     }
 
 public:
-    hop_match_fn(buffer<optional<expr>> & subst, name_generator const & ngen, name_map<name> * name_subst, hop_matcher_plugin const * plugin):
+    match_fn(buffer<optional<expr>> & subst, name_generator const & ngen, name_map<name> * name_subst, matcher_plugin const * plugin):
         m_subst(subst), m_ngen(ngen), m_name_subst(name_subst), m_plugin(plugin) {}
 
     bool match(expr const & p, expr const & t) {
@@ -157,16 +157,16 @@ public:
 };
 
 static name g_tmp_prefix = name::mk_internal_unique_name();
-bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst, name const * prefix,
-               name_map<name> * name_subst, hop_matcher_plugin const * plugin) {
+bool match(expr const & p, expr const & t, buffer<optional<expr>> & subst, name const * prefix,
+               name_map<name> * name_subst, matcher_plugin const * plugin) {
     lean_assert(closed(t));
     if (prefix)
-        return hop_match_fn(subst, name_generator(*prefix), name_subst, plugin).match(p, t);
+        return match_fn(subst, name_generator(*prefix), name_subst, plugin).match(p, t);
     else
-        return hop_match_fn(subst, name_generator(g_tmp_prefix), name_subst, plugin).match(p, t);
+        return match_fn(subst, name_generator(g_tmp_prefix), name_subst, plugin).match(p, t);
 }
 
-static int hop_match(lua_State * L) {
+static int match(lua_State * L) {
     expr p     = to_expr(L, 1);
     expr t     = to_expr(L, 2);
     if (!closed(t))
@@ -174,7 +174,7 @@ static int hop_match(lua_State * L) {
     unsigned k = get_free_var_range(p);
     buffer<optional<expr>> subst;
     subst.resize(k);
-    if (hop_match(p, t, subst, nullptr, nullptr, nullptr)) {
+    if (match(p, t, subst, nullptr, nullptr, nullptr)) {
         lua_newtable(L);
         int i = 1;
         for (auto s : subst) {
@@ -191,7 +191,7 @@ static int hop_match(lua_State * L) {
     return 1;
 }
 
-void open_hop_match(lua_State * L) {
-    SET_GLOBAL_FUN(hop_match, "match");
+void open_match(lua_State * L) {
+    SET_GLOBAL_FUN(match, "match");
 }
 }
diff --git a/src/library/hop_match.h b/src/library/match.h
similarity index 84%
rename from src/library/hop_match.h
rename to src/library/match.h
index ecb910e5e..e5fd01a23 100644
--- a/src/library/hop_match.h
+++ b/src/library/match.h
@@ -19,7 +19,7 @@ namespace lean {
 
     plugin(p, t, s) must return true iff for updated substitution s', s'(p) is definitionally equal to t.
 */
-typedef std::function<bool(expr const &, expr const &, buffer<optional<expr>> &, name_generator const &)> hop_matcher_plugin; // NOLINT
+typedef std::function<bool(expr const &, expr const &, buffer<optional<expr>> &, name_generator const &)> matcher_plugin; // NOLINT
 
 /**
    \brief Matching for higher-order patterns. Return true iff \c t matches the higher-order pattern \c p.
@@ -45,7 +45,7 @@ typedef std::function<bool(expr const &, expr const &, buffer<optional<expr>> &,
 
    If the plugin is provided, then it is invoked before a failure.
 */
-bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst, name const * prefix = nullptr,
-               name_map<name> * name_subst = nullptr, hop_matcher_plugin const * plugin = nullptr);
-void open_hop_match(lua_State * L);
+bool match(expr const & p, expr const & t, buffer<optional<expr>> & subst, name const * prefix = nullptr,
+               name_map<name> * name_subst = nullptr, matcher_plugin const * plugin = nullptr);
+void open_match(lua_State * L);
 }
diff --git a/src/library/register_module.h b/src/library/register_module.h
index 0c2f8f2ce..62efd1eec 100644
--- a/src/library/register_module.h
+++ b/src/library/register_module.h
@@ -16,7 +16,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/unifier.h"
 #include "library/scoped_ext.h"
-#include "library/hop_match.h"
+#include "library/match.h"
 
 namespace lean {
 inline void open_core_module(lua_State * L) {
@@ -30,7 +30,7 @@ inline void open_core_module(lua_State * L) {
     open_scoped_ext(L);
     open_unifier(L);
     open_explicit(L);
-    open_hop_match(L);
+    open_match(L);
 }
 inline void register_core_module() {
     script_state::register_module(open_core_module);