diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 17b6ef0f4..231d193c3 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -186,18 +186,16 @@ expr substitution::instantiate_metavars_wo_jst(expr const & e) {
     return instantiate_metavars_fn(*this, false)(e);
 }
 
-bool substitution::occurs_expr(name const & m, expr const & e) const {
+bool substitution::occurs_expr(name const & m, expr const & e) {
     if (!has_expr_metavar(e))
         return false;
+    expr new_e = instantiate(e);
     bool found = false;
-    for_each(e, [&](expr const & e, unsigned) {
+    for_each(new_e, [&](expr const & e, unsigned) {
             if (found || !has_expr_metavar(e)) return false;
             if (is_metavar(e)) {
                 if (mlocal_name(e) == m)
                     found = true;
-                auto s = get_expr(e);
-                if (s && occurs_expr(m, *s))
-                    found = true;
                 return false; // do not visit type
             }
             if (is_local(e)) return false; // do not visit type
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index c1663cf06..c90466e9e 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -78,7 +78,7 @@ public:
     expr instantiate(expr const & e) { return instantiate_metavars_wo_jst(e); }
 
     /** \brief Return true iff the metavariable \c m occurrs (directly or indirectly) in \c e. */
-    bool occurs_expr(name const & m, expr const & e) const;
-    bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); }
+    bool occurs_expr(name const & m, expr const & e);
+    bool occurs(expr const & m, expr const & e) { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); }
 };
 }
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 881a9badf..062ae0216 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -70,7 +70,7 @@ bool context_check(expr const & e, buffer<expr> const & locals) {
 //     constants are in \c e are in \c locals.
 //   - l_false if \c e contains \c m or it contains a local constant \c l
 //     not in locals that is not in a metavariable application.
-lbool occurs_context_check(substitution const & s, expr const & e, expr const & m, buffer<expr> const & locals) {
+lbool occurs_context_check(substitution & s, expr const & e, expr const & m, buffer<expr> const & locals) {
     expr root = e;
     lbool r = l_true;
     for_each(e, [&](expr const & e, unsigned) {
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index 9d92b409e..7958a0f85 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -91,11 +91,14 @@ static void tst2() {
     expr f = Const("f");
     expr g = Const("g");
     expr a = Const("a");
+    lean_assert(s.occurs(m1, f(m1)));
+    lean_assert(!s.occurs(m2, f(m1)));
     s.assign(m1, f(m2), mk_assumption_justification(1));
+    lean_assert(s.occurs(m2, f(m1)));
     s.assign(m2, g(a),  mk_assumption_justification(2));
     lean_assert(check_assumptions(s.get_assignment(m1)->second, {1}));
-    lean_assert(s.occurs(m1, f(m1)));
-    lean_assert(s.occurs(m2, f(m1)));
+    lean_assert(!s.occurs(m1, f(m1)));
+    lean_assert(!s.occurs(m2, f(m1)));
     lean_assert(!s.occurs(m1, f(m2)));
     lean_assert(!s.occurs(m1, f(a)));
     lean_assert(!s.occurs(m3, f(m1)));
diff --git a/tests/lua/subst1.lua b/tests/lua/subst1.lua
index b450ad372..f26ddadd2 100644
--- a/tests/lua/subst1.lua
+++ b/tests/lua/subst1.lua
@@ -24,8 +24,8 @@ assert(s:get_expr("m") == a)
 local m2 = mk_metavar("m2", Prop)
 s:assign(m2, f(m))
 print(s:get_expr("m2"))
-assert(s:occurs(m, f(m2)))
-assert(s:occurs_expr("m", f(m2)))
+assert(not s:occurs(m, f(m2)))
+assert(not s:occurs_expr("m", f(m2)))
 print(s:get_level("u"))
 print(s:instantiate(mk_sort(u)))
 assert(s:instantiate(mk_sort(u)) == mk_sort(l))