From 6f74f6522084926490b7d76794c589554fc3a83a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Mar 2016 13:37:33 -0700
Subject: [PATCH] fix(library/type_context): instantiate was not replacing all
 assigned metavars

---
 src/library/type_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 32e94be26..38222d893 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -590,7 +590,7 @@ struct instantiate_uvars_mvars_fn : public replace_visitor {
     virtual expr visit_meta(expr const & m) override {
         if (m_owner.is_mvar(m)) {
             if (auto v1 = m_owner.get_assignment(m)) {
-                if (!has_expr_metavar(*v1)) {
+                if (!has_metavar(*v1)) {
                     return *v1;
                 } else {
                     expr v2 = m_owner.instantiate_uvars_mvars(*v1);