diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index cd14e775e..7975eb346 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -295,6 +295,7 @@ static bool all_unassigned(substitution const & subst, name_set const & s) {
 
 name_set substitution::get_occs(name const & m, name_set & fresh) {
     lean_assert(is_expr_assigned(m));
+    check_system("substitution occurs check");
     if (fresh.contains(m)) {
         return *m_occs_map.find(m);
     } else if (name_set const * it = m_occs_map.find(m)) {