From fc01edee4da780bd188e69db4fbc32e696cbdb05 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Oct 2014 17:53:24 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): perform translation using
 "user-level" names

---
 src/frontends/lean/elaborator.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e93cdf979..9395177c0 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1128,7 +1128,7 @@ std::tuple<expr, expr, level_param_names> elaborator::operator()(
 static expr translate_local_name(environment const & env, list<expr> const & ctx, name const & local_name,
                                  expr const & src) {
     for (expr const & local : ctx) {
-        if (mlocal_name(local) == local_name)
+        if (local_pp_name(local) == local_name)
             return local;
     }
     // TODO(Leo): we should create an elaborator exception.
@@ -1151,7 +1151,7 @@ static expr translate(environment const & env, list<expr> const & ctx, expr cons
                 return none_expr();
             }
         } else if (is_local(e)) {
-            return some_expr(translate_local_name(env, ctx, mlocal_name(e), e));
+            return some_expr(translate_local_name(env, ctx, local_pp_name(e), e));
         } else {
             return none_expr();
         }