From 376126241e0c519dadfd19a7b6752b348db57dcd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 3 Jan 2015 15:29:34 -0800
Subject: [PATCH] fix(library/definitional/equations): typo and bug

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

diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp
index 47328268f..ee35c93b7 100644
--- a/src/library/definitional/equations.cpp
+++ b/src/library/definitional/equations.cpp
@@ -867,7 +867,7 @@ class equation_compiler_fn {
 
     /** \brief Return true iff \c t1 and \c t2 are instances of the same inductive datatype */
     static bool is_same_inductive(expr const & t1, expr const & t2) {
-        return const_name(get_app_fn(t1)) != const_name(get_app_fn(t2));
+        return const_name(get_app_fn(t1)) == const_name(get_app_fn(t2));
     }
 
     /** \brief Return true iff \c s is structurally smaller than \c t OR equal to \c t */
@@ -929,6 +929,8 @@ class equation_compiler_fn {
                                 // arg_j must be structurally smaller than arg
                                 if (!m_main.is_lt(arg_j, arg))
                                     return false;
+                            } else {
+                                return false;
                             }
                             break;
                         }