From d1c645977d0418e47657eb2e8b11aebfa511cf0e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 14 Aug 2014 10:53:22 -0700
Subject: [PATCH] fix(frontends/lean/info_manager): add missing method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/info_manager.cpp | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index 492d05855a..24f3ef6207 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -132,7 +132,18 @@ void info_manager::append(std::vector<std::unique_ptr<info_data>> && vs, bool re
     }
 }
 
-void info_manager::append(std::vector<type_info_data> & v, bool remove_duplicates) {
+void info_manager::append(std::vector<type_info_data> & vs, bool remove_duplicates) {
+    lock_guard<mutex> lc(m_mutex);
+    std::stable_sort(vs.begin(), vs.end());
+    type_info_data prev;
+    bool first = true;
+    for (auto & v : vs) {
+        if (!remove_duplicates || first || !v.eq_pos(prev.get_line(), prev.get_column())) {
+            prev = v;
+            add_core(std::unique_ptr<info_data>(new type_info_data(v)));
+            first = false;
+        }
+    }
 }
 
 void info_manager::sort() {