From f47e1bed01f7737288a7b1765ce631af28ff8564 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Feb 2015 18:21:32 -0800
Subject: [PATCH] feat(library/abbreviation): store inverse map ignoring
 universe level parameters

---
 src/library/abbreviation.cpp | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp
index a408328a8..76cbb5651 100644
--- a/src/library/abbreviation.cpp
+++ b/src/library/abbreviation.cpp
@@ -16,16 +16,17 @@ namespace lean {
 typedef pair<name, bool> abbrev_entry;
 
 struct abbrev_state {
-    name_map<bool>                     m_abbrevs;
-    rb_map<expr, name, expr_quick_cmp> m_inv_map; // for pretty printer
+    name_map<bool>                               m_abbrevs;
+    rb_map<expr, name, expr_cmp_no_level_params> m_inv_map; // for pretty printer
 
     void add(environment const & env, name const & n, bool parsing_only) {
         declaration const & d = env.get(n);
         if (!d.is_definition())
             throw exception(sstream() << "invalid abbreviation '" << n << "', it is not a definition");
         m_abbrevs.insert(n, parsing_only);
-        if (!parsing_only)
+        if (!parsing_only) {
             m_inv_map.insert(d.get_value(), n);
+        }
     }
 
     bool is_abbreviation(name const & n) const { return m_abbrevs.contains(n); }