From 58b6169e8bb5979ebdbfa8e8a26f9e0bf15d3a90 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 28 Jun 2014 08:31:09 -0700
Subject: [PATCH] fix(library/max_sharing): take binder annotations into
 account

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

diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index 5e5c53eb83..43e8744a1d 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -17,7 +17,7 @@ namespace lean {
    shared sub-expressions.
 */
 struct max_sharing_fn::imp {
-    typedef typename std::unordered_set<expr, expr_hash, std::equal_to<expr>> expr_cache;
+    typedef typename std::unordered_set<expr, expr_hash, is_bi_equal_proc> expr_cache;
 
     expr_cache m_cache;