From 45e62031e20aeff2ebe19320c75009b515ca39d4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Feb 2015 13:28:57 -0800
Subject: [PATCH] fix(library/match): bug in matcher

---
 src/library/match.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/library/match.cpp b/src/library/match.cpp
index f1472b9c01..31b530672a 100644
--- a/src/library/match.cpp
+++ b/src/library/match.cpp
@@ -311,8 +311,6 @@ class match_fn : public match_context {
             auto s = _get_subst(p);
             if (s) {
                 return match_core(*s, t);
-            } else if (has_local(t)) {
-                return false;
             } else {
                 _assign(p, t);
                 return true;