diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index da7163320..6850fec27 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -6,7 +6,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   update_declaration.cpp choice.cpp scoped_ext.cpp locals.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)
+  explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
+  hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/hop_match.cpp b/src/library/hop_match.cpp
index ccde9e194..abdd00b77 100644
--- a/src/library/hop_match.cpp
+++ b/src/library/hop_match.cpp
@@ -1,373 +1,187 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "util/optional.h"
-#include "util/buffer.h"
-#include "kernel/free_vars.h"
+#include "kernel/abstract.h"
 #include "kernel/instantiate.h"
-#include "kernel/kernel.h"
-#include "kernel/for_each_fn.h"
-#include "kernel/replace_visitor.h"
-#include "library/equality.h"
 #include "library/kernel_bindings.h"
+#include "library/locals.h"
 #include "library/hop_match.h"
 
 namespace lean {
-
 class hop_match_fn {
-    buffer<optional<expr>> & m_subst;
-    buffer<expr>             m_vars;
-    optional<ro_environment> m_env;
-    optional<ro_metavar_env> m_menv;
-    name_map<name> *         m_name_subst;
+    buffer<optional<expr>> &   m_subst;
+    name_generator             m_ngen;
+    name_map<name> *           m_name_subst;
+    hop_matcher_plugin const * m_plugin;
 
-    bool is_free_var(expr const & x, unsigned ctx_size) const {
-        return is_var(x) && var_idx(x) >= ctx_size;
+    void assign(expr const & p, expr const & t) {
+        lean_assert(var_idx(p) < m_subst.size());
+        unsigned vidx = var_idx(p);
+        unsigned sz   = m_subst.size();
+        m_subst[sz - vidx - 1] = t;
     }
 
-    bool is_locally_bound(expr const & x, unsigned ctx_size) const {
-        return is_var(x) && var_idx(x) < ctx_size;
-    }
-
-    expr lift_free_vars(expr const & e, unsigned d) const { return ::lean::lift_free_vars(e, d, m_menv); }
-    expr lower_free_vars(expr const & e, unsigned s, unsigned d) const { return ::lean::lower_free_vars(e, s, d, m_menv); }
-    bool has_free_var(expr const & e, unsigned i) const { return ::lean::has_free_var(e, i, m_menv); }
-    bool has_free_var(expr const & e, unsigned low, unsigned high) const { return ::lean::has_free_var(e, low, high, m_menv); }
-    expr apply_beta(expr f, unsigned num_args, expr const * args) const { return ::lean::apply_beta(f, num_args, args, m_menv); }
-    bool has_free_var_ge(expr const & e, unsigned low) const { return ::lean::has_free_var_ge(e, low, m_menv); }
-
-    optional<expr> get_subst(expr const & x, unsigned ctx_size) const {
-        lean_assert(is_free_var(x, ctx_size));
-        unsigned vidx = var_idx(x) - ctx_size;
+    optional<expr> get_subst(expr const & x) const {
+        unsigned vidx = var_idx(x);
         unsigned sz = m_subst.size();
         if (vidx >= sz)
             throw exception("ill-formed higher-order matching problem");
         return m_subst[sz - vidx - 1];
     }
 
-    bool has_locally_bound_var(expr const & t, unsigned ctx_size) const {
-        return has_free_var(t, 0, ctx_size);
-    }
-
-    void assign(expr const & p, expr const & t, unsigned ctx_size) {
-        lean_assert(is_free_var(p, ctx_size));
-        lean_assert(!get_subst(p, ctx_size));
-        unsigned vidx = var_idx(p) - ctx_size;
-        unsigned sz = m_subst.size();
-        m_subst[sz - vidx - 1] = t;
-    }
-
-    bool args_are_distinct_locally_bound_vars(expr const & p, unsigned ctx_size, buffer<expr> & vars) {
-        lean_assert(is_app(p));
-        vars.clear();
-        unsigned num = num_args(p);
-        for (unsigned i = 1; i < num; i++) {
-            expr const & v = arg(p, i);
-            if (!is_locally_bound(v, ctx_size))
+    bool args_are_distinct_locals(buffer<expr> const & args) {
+        for (auto it = args.begin(); it != args.end(); it++) {
+            if (!is_local(*it) || contains_local(*it, args.begin(), it))
                 return false;
-            if (std::find(vars.begin(), vars.end(), v) != vars.end())
-                return false;
-            vars.push_back(v);
         }
         return true;
     }
 
-    /**
-       \brief Return t' when all locally bound variables in \c t occur in vars at positions [0, vars_size).
-       The locally bound variables occurring in \c t are replaced using the following mapping:
-
-             vars[vars_size - 1] ==> #0
-             ...
-             vars[0]             ==> #vars_size - 1
-
-       None is returned if \c t contains a locally bound variable that does not occur in \c vars.
-       Remark: vars_size <= vars.size()
-     */
-    optional<expr> proj_core(expr const & t, unsigned ctx_size, buffer<expr> const & vars, unsigned vars_size) {
-        bool failed = false;
-        expr r = replace(t, [&](expr const & e, unsigned offset) -> expr {
-                if (is_var(e)) {
-                    unsigned vidx = var_idx(e);
-                    if (vidx < offset)
-                        return e;
-                    vidx -= offset;
-                    if (vidx < ctx_size) {
-                        // e is locally bound
-                        for (unsigned i = 0; i < vars_size; i++) {
-                            if (var_idx(vars[i]) == vidx)
-                                return mk_var(offset + vars_size - i - 1);
-                        }
-                        failed = true;
-                        return e;
-                    } else if (ctx_size != vars_size) {
-                        return mk_var(offset + vidx - ctx_size + vars_size);
-                    } else {
-                        return e;
-                    }
-                } else {
-                    return e;
-                }
-            });
-        if (failed)
+    optional<expr> proj(expr const & t, buffer<expr> const & args) {
+        expr r = Fun(args, t);
+        if (has_local(r))
             return none_expr();
         else
             return some_expr(r);
     }
 
-    // We say \c t has a simple projection when it is of the form (f v1 ... vn)
-    // where f does no contain locally bound variables, and v1 ... vn are exactly the variables in vars.
-    // In this case, the proj procedure can return f instead of (fun xn .... x1, f x1 ... xn)
-    bool is_simple_proj(expr const & t, unsigned ctx_size, buffer<expr> const & vars) {
-        if (is_app(t) && !has_locally_bound_var(arg(t, 0), ctx_size) && num_args(t) == vars.size() + 1) {
-            for (unsigned i = 0; i < vars.size(); i++)
-                if (arg(t, i+1) != vars[i])
-                    return false;
-            return true;
-        } else {
+    bool match_plugin(expr const & p, expr const & t) {
+        if (!m_plugin)
             return false;
-        }
+        return (*m_plugin)(p, t, m_subst, m_ngen.mk_child());
     }
 
-    /**
-       \brief Return <tt>(fun (x1 ... xn) t')</tt> if all locally bound variables in \c t occur in vars.
-       \c n is the size of \c vars.
-       None is returned if \c t contains a locally bound variable that does not occur in \c vars.
-    */
-    optional<expr> proj(expr const & t, context const & ctx, unsigned ctx_size, buffer<expr> const & vars) {
-        if (is_simple_proj(t, ctx_size, vars)) {
-            return some_expr(lower_free_vars(arg(t, 0), ctx_size, ctx_size));
+    bool match_binding(expr p, expr t) {
+        lean_assert(is_binding(p) && is_binding(t));
+        buffer<expr>  ls;
+        expr_kind k = p.kind();
+        while (p.kind() == k && t.kind() == k) {
+            if (m_name_subst)
+                (*m_name_subst)[binding_name(p)] = binding_name(t);
+            expr p_d  = instantiate_rev(binding_domain(p), ls.size(), ls.data());
+            expr t_d  = instantiate_rev(binding_domain(t), ls.size(), ls.data());
+            if (!match(p_d, t_d))
+                return false;
+            expr l  = mk_local(m_ngen.next(), binding_name(t), t_d, binding_info(t));
+            ls.push_back(l);
+            p = binding_body(p);
+            t = binding_body(t);
         }
-        optional<expr> t_prime = proj_core(t, ctx_size, vars, vars.size());
-        if (!t_prime)
-            return none_expr();
-        expr r     = *t_prime;
-        unsigned i = vars.size();
-        while (i > 0) {
-            --i;
-            unsigned vidx = var_idx(vars[i]);
-            auto p = lookup_ext(ctx, vidx);
-            context_entry const & entry = p.first;
-            context entry_ctx = p.second;
-            if (!entry.get_domain())
-                return none_expr();
-            expr d     = *entry.get_domain();
-            optional<expr> new_d = proj_core(d, entry_ctx.size(), vars, i);
-            if (!new_d)
-                return none_expr();
-            r = mk_lambda(entry.get_name(), *new_d, r);
-        }
-        return some_expr(r);
+        if (p.kind() == k || t.kind() == k)
+            return false;
+        p = instantiate_rev(p, ls.size(), ls.data());
+        t = instantiate_rev(t, ls.size(), ls.data());
+        return match(p, t);
     }
 
-    optional<expr> unfold_constant(expr const & c) {
-        if (is_constant(c)) {
-            auto obj = (*m_env)->find_object(const_name(c));
-            if (obj && (obj->is_definition() || obj->is_builtin()))
-                return some_expr(obj->get_value());
-        }
-        return none_expr();
-    }
-
-    bool match_constant(expr const & p, expr const & t) {
-        if (p == t)
+    bool match_macro(expr const & p, expr const & t) {
+        if (macro_def(p) == macro_def(t) && macro_num_args(p) == macro_num_args(t)) {
+            for (unsigned i = 0; i < macro_num_args(p); i++) {
+                if (!match(macro_arg(p, i), macro_arg(t, i)))
+                    return false;
+            }
             return true;
-        auto new_p = unfold_constant(p);
-        if (new_p)
-            return match_constant(*new_p, t);
+        }
         return false;
     }
 
-    /**
-       \brief Return true iff all free variables in the pattern \c p are assigned.
-    */
-    bool all_free_vars_are_assigned(expr const & p, unsigned ctx_size) const {
-        bool result = true;
-        for_each(p, [&](expr const & v, unsigned offset) {
-                if (!result)
-                    return false;
-                if (is_var(v) && this->is_free_var(v, ctx_size + offset) && !get_subst(v, ctx_size + offset)) {
-                    result = false;
-                }
-                return true;
-            });
-        return result;
+    bool match_app(expr const & p, expr const & t) {
+        return match_core(app_fn(p), app_fn(t)) && match(app_arg(p), app_arg(t));
     }
 
-    /**
-       \brief Auxiliary functional object for instantiating the free variables in a pattern.
-    */
-    class instantiate_free_vars_proc : public replace_visitor {
-    protected:
-        hop_match_fn &  m_ref;
-        unsigned        m_ctx_size;
-
-        virtual expr visit_var(expr const & x, context const & ctx) {
-            unsigned real_ctx_sz = ctx.size() + m_ctx_size;
-            if (m_ref.is_free_var(x, real_ctx_sz)) {
-                optional<expr> r = m_ref.get_subst(x, real_ctx_sz);
-                lean_assert(r);
-                return m_ref.lift_free_vars(*r, real_ctx_sz);
-            } else {
-                return x;
-            }
+    bool match_core(expr const & p, expr const & t) {
+        if (p.kind() != t.kind())
+            return match_plugin(p, t);
+        switch (p.kind()) {
+        case expr_kind::Local: case expr_kind::Meta:
+            return mlocal_name(p) == mlocal_name(t);
+        case expr_kind::Var:
+            lean_unreachable(); // LCOV_EXCL_LINE
+        case expr_kind::Constant:
+            // TODO(Leo): universe levels
+            return const_name(p) == const_name(t);
+        case expr_kind::Sort:
+            // TODO(Leo): universe levels
+            return true;
+        case expr_kind::Lambda: case expr_kind::Pi:
+            return match_binding(p, t) || match_plugin(p, t);
+        case expr_kind::Macro:
+            return match_macro(p, t) || match_plugin(p, t);
+        case expr_kind::App:
+            return match_app(p, t) || match_plugin(p, t);
         }
+        lean_unreachable(); // LCOV_EXCL_LINE
+    }
 
-        virtual expr visit_app(expr const & e, context const & ctx) {
-            unsigned real_ctx_sz = ctx.size() + m_ctx_size;
-            expr const & f = arg(e, 0);
-            if (is_var(f) && m_ref.is_free_var(f, real_ctx_sz)) {
-                buffer<expr> new_args;
-                for (unsigned i = 0; i < num_args(e); i++)
-                    new_args.push_back(visit(arg(e, i), ctx));
-                if (is_lambda(new_args[0]))
-                    return m_ref.apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1);
-                else
-                    return mk_app(new_args);
-            } else {
-                return replace_visitor::visit_app(e, ctx);
-            }
-        }
+public:
+    hop_match_fn(buffer<optional<expr>> & subst, name_generator const & ngen, name_map<name> * name_subst, hop_matcher_plugin const * plugin):
+        m_subst(subst), m_ngen(ngen), m_name_subst(name_subst), m_plugin(plugin) {}
 
-    public:
-        instantiate_free_vars_proc(hop_match_fn & fn, unsigned ctx_size):
-            m_ref(fn), m_ctx_size(ctx_size) {
-        }
-    };
-
-    bool match(expr const & p, expr const & t, context const & ctx, unsigned ctx_size) {
-        lean_assert(ctx.size() == ctx_size);
-        if (is_free_var(p, ctx_size)) {
-            auto s = get_subst(p, ctx_size);
+    bool match(expr const & p, expr const & t) {
+        if (is_var(p)) {
+            auto s = get_subst(p);
             if (s) {
-                return lift_free_vars(*s, ctx_size) == t;
-            } else if (has_locally_bound_var(t, ctx_size)) {
+                return match_core(*s, t);
+            } else if (has_local(t)) {
                 return false;
             } else {
-                assign(p, lower_free_vars(t, ctx_size, ctx_size), ctx_size);
+                assign(p, t);
                 return true;
             }
-        } else if (is_app(p) && is_free_var(arg(p, 0), ctx_size)) {
-            if (args_are_distinct_locally_bound_vars(p, ctx_size, m_vars)) {
+        } else if (is_app(p)) {
+            buffer<expr> args;
+            expr const & f = get_app_rev_args(p, args);
+            if (is_var(f)) {
                 // higher-order pattern case
-                auto s = get_subst(arg(p, 0), ctx_size);
-                unsigned num = num_args(p);
+                auto s = get_subst(f);
                 if (s) {
-                    expr f     = lift_free_vars(*s, ctx_size);
-                    expr new_p = apply_beta(f, num - 1, &(arg(p, 1)));
-                    return new_p == t;
-                } else {
-                    optional<expr> new_t = proj(t, ctx, ctx_size, m_vars);
+                    expr new_p = apply_beta(*s, args.size(), args.data());
+                    return match_core(new_p, t);
+                }
+                if (args_are_distinct_locals(args)) {
+                    optional<expr> new_t = proj(t, args);
                     if (new_t) {
-                        assign(arg(p, 0), *new_t, ctx_size);
+                        assign(f, *new_t);
                         return true;
                     }
                 }
-            } else if (all_free_vars_are_assigned(p, ctx_size)) {
-                instantiate_free_vars_proc proc(*this, ctx_size);
-                expr new_p = proc(p);
-                return new_p == t;
             }
             // fallback to the first-order case
         }
 
-        if (p == t && !has_free_var_ge(p, ctx_size)) {
-            return true;
-        }
-
-        if (m_env && is_constant(p)) {
-            return match_constant(p, t);
-        }
-
-        if (p.kind() != t.kind())
-            return false;
-        switch (p.kind()) {
-        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type:
-        case expr_kind::Value: case expr_kind::MetaVar:
-            return false;
-        case expr_kind::App: {
-            unsigned i1 = num_args(p);
-            unsigned i2 = num_args(t);
-            while (i1 > 0 && i2 > 0) {
-                --i1;
-                --i2;
-                if (i1 == 0 && i2 > 0) {
-                    return match(arg(p, i1), mk_app(i2+1, begin_args(t)), ctx, ctx_size);
-                } else if (i2 == 0 && i1 > 0) {
-                    return match(mk_app(i1+1, begin_args(p)), arg(t, i2), ctx, ctx_size);
-                } else {
-                    if (!match(arg(p, i1), arg(t, i2), ctx, ctx_size))
-                        return false;
-                }
-            }
-            return true;
-        }
-        case expr_kind::Proj:
-            return proj_first(p) == proj_first(t) && match(proj_arg(p), proj_arg(t), ctx, ctx_size);
-        case expr_kind::HEq:
-            return
-                match(heq_lhs(p), heq_lhs(t), ctx, ctx_size) &&
-                match(heq_rhs(p), heq_rhs(t), ctx, ctx_size);
-        case expr_kind::Pair:
-            return
-                match(pair_first(p),  pair_first(t), ctx, ctx_size) &&
-                match(pair_second(p), pair_second(t), ctx, ctx_size) &&
-                match(pair_type(p),   pair_type(t), ctx, ctx_size);
-        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma:
-            if (m_name_subst)
-                (*m_name_subst)[abst_name(p)] = abst_name(t);
-            return
-                match(abst_domain(p), abst_domain(t), ctx, ctx_size) &&
-                match(abst_body(p), abst_body(t), extend(ctx, abst_name(t), abst_domain(t)), ctx_size+1);
-        case expr_kind::Let:
-            // TODO(Leo)
-            return false;
-        }
-        lean_unreachable();
-    }
-public:
-    hop_match_fn(buffer<optional<expr>> & subst, optional<ro_environment> const & env,
-                 optional<ro_metavar_env> const & menv, name_map<name> * name_subst):
-        m_subst(subst), m_env(env), m_menv(menv), m_name_subst(name_subst) {}
-
-    bool operator()(expr const & p, expr const & t) {
-        return match(p, t, context(), 0);
+        return match_core(p, t);
     }
 };
 
-bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst, optional<ro_environment> const & env,
-               optional<ro_metavar_env> const & menv, name_map<name> * name_subst) {
-    return hop_match_fn(subst, env, menv, name_subst)(p, t);
+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) {
+    lean_assert(closed(t));
+    if (prefix)
+        return hop_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);
 }
 
-static int hop_match_core(lua_State * L, optional<ro_environment> const & env) {
-    int nargs = lua_gettop(L);
-    expr p    = to_expr(L, 1);
-    expr t    = to_expr(L, 2);
-    int k     = 0;
-    optional<ro_metavar_env> menv;
-    if (nargs >= 4 && !lua_isnil(L, 4))
-        menv = to_metavar_env(L, 4);
-    if (nargs >= 5) {
-        k = luaL_checkinteger(L, 5);
-        if (k < 0)
-            throw exception("hop_match, arg #4 must be non-negative");
-    } else {
-        k = free_var_range(p);
-    }
+static int hop_match(lua_State * L) {
+    expr p     = to_expr(L, 1);
+    expr t     = to_expr(L, 2);
+    if (!closed(t))
+        throw exception("higher-order pattern matching failure, input term must not contain free variables");
+    unsigned k = get_free_var_range(p);
     buffer<optional<expr>> subst;
     subst.resize(k);
-    if (hop_match(p, t, subst, env, menv)) {
+    if (hop_match(p, t, subst, nullptr, nullptr, nullptr)) {
         lua_newtable(L);
         int i = 1;
         for (auto s : subst) {
-            if (s) {
+            if (s)
                 push_expr(L, *s);
-            } else {
+            else
                 lua_pushboolean(L, false);
-            }
             lua_rawseti(L, -2, i);
             i = i + 1;
         }
@@ -377,22 +191,7 @@ static int hop_match_core(lua_State * L, optional<ro_environment> const & env) {
     return 1;
 }
 
-static int hop_match(lua_State * L) {
-    int nargs = lua_gettop(L);
-    if (nargs >= 3) {
-        if (!lua_isnil(L, 3)) {
-            ro_shared_environment env(L, 3);
-            return hop_match_core(L, optional<ro_environment>(env));
-        } else {
-            return hop_match_core(L, optional<ro_environment>());
-        }
-    } else {
-        ro_shared_environment env(L);
-        return hop_match_core(L, optional<ro_environment>(env));
-    }
-}
-
 void open_hop_match(lua_State * L) {
-    SET_GLOBAL_FUN(hop_match, "hop_match");
+    SET_GLOBAL_FUN(hop_match, "match");
 }
 }
diff --git a/src/library/hop_match.h b/src/library/hop_match.h
index 75f5b0f41..ecb910e5e 100644
--- a/src/library/hop_match.h
+++ b/src/library/hop_match.h
@@ -1,44 +1,51 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
 #pragma once
+#include <functional>
 #include "util/lua.h"
+#include "util/optional.h"
+#include "util/buffer.h"
+#include "util/name_map.h"
 #include "kernel/expr.h"
 #include "kernel/environment.h"
 
 namespace lean {
+/** \brief Callback for extending the higher-order pattern matching procedure.
+    It is invoked before the matcher fails.
+
+    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
+
 /**
    \brief Matching for higher-order patterns. Return true iff \c t matches the higher-order pattern \c p.
-   The substitution is stored in \c subst.
+   The substitution is stored in \c subst. Note that, this procedure treats free-variables as placholders
+   instead of meta-variables.
 
    \c subst is an assignment for the free variables occurring in \c p.
 
-   The free variables occurring in \c t are treated as constants.
-
-   We say non-free variables occurring in \c p and \c t are "locally bound".
+   \pre \c t must not contain free variables. If it does, they must be replaced with local constants
+   before invoking this functions.
 
    \c p is a higher-order pattern when in all applications in \c p
       1- A free variable is not the function OR
-      2- A free variable is the function, but all other arguments are distinct locally bound variables.
+      2- A free variable is the function, but all other arguments are distinct local constants.
 
    \pre \c subst must be big enough to store all free variables occurring in subst
 
-   If an environment is provided, then a constant \c c matches a term \c t if
-   \c c is definitionally equal to \c t.
-
-   If a metavariable environment is provided, then it is provided to lift/lower
-   free variables procedures to be able to minimize the size of the local context.
+   If prefix is provided, then it is used for creating unique names.
 
    If name_subst is different from nullptr, then the procedure stores in name_subst
    a mapping for binder names. It maps the binder names used in the pattern \c p into
    the binder names used in \c t.
+
+   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,
-               optional<ro_environment> const & env = optional<ro_environment>(),
-               optional<ro_metavar_env> const & menv = optional<ro_metavar_env>(),
-               name_map<name> * name_subst = nullptr);
+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);
 }
diff --git a/src/library/locals.h b/src/library/locals.h
index 5b7f83121..57d524959 100644
--- a/src/library/locals.h
+++ b/src/library/locals.h
@@ -12,4 +12,14 @@ namespace lean {
 name_set collect_univ_params(expr const & e, name_set const & ls = name_set());
 void collect_locals(expr const & e, expr_struct_set & ls);
 level_param_names to_level_param_names(name_set const & ls);
+
+/** \brief Return true iff \c [begin_locals, end_locals) contains \c local */
+template<typename It> bool contains_local(expr const & local, It const & begin_locals, It const & end_locals) {
+    return std::any_of(begin_locals, end_locals, [&](expr const & l) { return mlocal_name(local) == mlocal_name(l); });
+}
+
+/** \brief Return true iff \c locals contains \c local */
+inline bool contains_local(expr const & local, buffer<expr> const & locals) {
+    return contains_local(local, locals.begin(), locals.end());
+}
 }
diff --git a/src/library/register_module.h b/src/library/register_module.h
index 05efab159..0c2f8f2ce 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/hop_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_hop_match(L);
 }
 inline void register_core_module() {
     script_state::register_module(open_core_module);
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 60c5a63b9..1a9400ca7 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/error_msgs.h"
 #include "library/occurs.h"
+#include "library/locals.h"
 #include "library/unifier.h"
 #include "library/opaque_hints.h"
 #include "library/unifier_plugin.h"
@@ -32,16 +33,6 @@ static name g_unifier_expensive      {"unifier", "expensive"};
 RegisterBoolOption(g_unifier_expensive, LEAN_DEFAULT_UNIFIER_EXPENSIVE, "(unifier) enable/disable expensive (and more complete) procedure");
 bool get_unifier_expensive(options const & opts) { return opts.get_bool(g_unifier_expensive, LEAN_DEFAULT_UNIFIER_EXPENSIVE); }
 
-/** \brief Return true iff \c [begin_locals, end_locals) contains \c local */
-template<typename It> bool contains_local(expr const & local, It const & begin_locals, It const & end_locals) {
-    return std::any_of(begin_locals, end_locals, [&](expr const & l) { return mlocal_name(local) == mlocal_name(l); });
-}
-
-/** \brief Return true iff \c locals contains \c local */
-bool contains_local(expr const & local, buffer<expr> const & locals) {
-    return contains_local(local, locals.begin(), locals.end());
-}
-
 // If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where
 // l_1 ... l_n are distinct local variables, then return ?m, and store l_1 ... l_n in args.
 // Otherwise return none.
diff --git a/tests/lua/hop1.lua b/tests/lua/hop1.lua
new file mode 100644
index 000000000..39af7d5a3
--- /dev/null
+++ b/tests/lua/hop1.lua
@@ -0,0 +1,24 @@
+function tst_match(p, t)
+   local r   = match(p, t)
+   assert(r)
+   print("--------------")
+   for i = 1, #r do
+      print("  #" .. i .. " := " .. tostring(r[i]))
+   end
+end
+
+local env = environment()
+local N   = Const("N")
+local f   = Const("f")
+local a   = Const("a")
+local b   = Const("b")
+local x   = Local("x", N)
+local y   = Local("y", N)
+tst_match(f(Var(0), Var(0)), f(a, a))
+tst_match(f(Var(0), Var(1)), f(a, b))
+tst_match(Var(0)(x, y), f(x, f(x, y)))
+assert(not match(Var(0)(x, x), f(x, f(x, y))))
+assert(not match(Var(0)(x), f(x, y)))
+tst_match(Pi(x, y, Var(2)(x)), Pi(x, y, f(f(x))))
+tst_match(Fun(x, y, Var(2)(x)), Fun(x, y, f(f(x))))
+assert(match(Pi(x, Var(2)(x)), Pi(x, y, f(f(x)))))