From d69f8293375bc9980780af9ddf38b00df0103df8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Mar 2015 19:09:01 -0700
Subject: [PATCH] perf(kernel/justification): avoid redundant justification
 objects

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

diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp
index 7e94f0530..b21ac80fc 100644
--- a/src/kernel/justification.cpp
+++ b/src/kernel/justification.cpp
@@ -296,7 +296,7 @@ justification mk_composite(justification const & j1, justification const & j2, o
     return justification(new (get_ext_composite_allocator().allocate()) ext_composite_cell(j1, j2, fn, s));
 }
 justification mk_composite1(justification const & j1, justification const & j2) {
-    if (j1.is_none())
+    if (j1.is_none() || j1.raw() == j2.raw())
         return j2;
     if (j2.is_none())
         return j1;