From 2eb84c5f7401c7c284befee2efbcc68807acf1f1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 24 Jul 2014 11:38:43 -0700
Subject: [PATCH] fix(library/unifier): make sure we do not miss dependency

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/unifier.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 14c225b5b1..d2b526e3ee 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -100,7 +100,7 @@ lbool occurs_context_check(substitution & s, expr const & e, expr const & m, buf
                     if (s.occurs(m, e))
                         r = l_undef;
                 }
-                if (get_app_fn(e) == m)
+                if (mlocal_name(get_app_fn(e)) == mlocal_name(m))
                     r = l_false;
                 return false; // do not visit children
             } else {