From bbc4380a52f28b2d12355b1a91e004ae724e3a86 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 Aug 2014 19:02:30 -0700
Subject: [PATCH] fix(library/unifier): bug exposed by recent changes

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

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 2dfaaa6bc..aa7b03012 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -62,6 +62,8 @@ bool context_check(expr const & e, buffer<expr> const & locals) {
                 failed = true;
                 return false;
             }
+            if (is_metavar(e))
+                return false; // do not visit type
             return has_local(e);
         });
     return !failed;