From c30c0fa3b8802763ba84915c4363cd4ab9323142 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 25 Oct 2014 00:19:41 -0700
Subject: [PATCH] fix(kernel/metavar): avoid crash due to stack overflow,
 closes #253

---
 src/kernel/metavar.cpp | 1 +
 1 file changed, 1 insertion(+)

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)) {