From 37ad850455772cce7e1777903b6ceab3f29f2605 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Nov 2015 08:23:54 -0700
Subject: [PATCH] fix(library/type_context): improve on_is_def_eq_failure

---
 src/library/type_context.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index bf923cb33..dac103681 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1298,13 +1298,15 @@ optional<pair<expr, expr>> type_context::find_unsynth_metavar(expr const & e) {
 }
 
 bool type_context::on_is_def_eq_failure(expr & e1, expr & e2) {
-    if (is_app(e1) && is_app(e2)) {
+    if (is_app(e1)) {
         if (auto p1 = find_unsynth_metavar(e1)) {
             if (mk_nested_instance(p1->first, p1->second)) {
                 e1 = instantiate_uvars_mvars(e1);
                 return true;
             }
         }
+    }
+    if (is_app(e2)) {
         if (auto p2 = find_unsynth_metavar(e2)) {
             if (mk_nested_instance(p2->first, p2->second)) {
                 e2 = instantiate_uvars_mvars(e2);