diff --git a/doc/server.org b/doc/server.org
index db06eb10e..a170c20e5 100644
--- a/doc/server.org
+++ b/doc/server.org
@@ -159,7 +159,6 @@ num → num
 num
 -- ACK
 -- IDENTIFIER|15|42
-f
 foo.f
 -- ACK
 -- ENDINFO
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 18d8b6337..8dac8c305 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -374,6 +374,8 @@ class elaborator {
         virtual optional<constraints> next() {
             while (m_idx < get_num_choices(m_choice)) {
                 expr const & c = get_choice(m_choice, m_idx);
+                expr const & f = get_app_fn(c);
+                m_elab.save_identifier_info(f);
                 m_idx++;
                 try {
                     new_scope s(m_elab, m_ctx, m_full_ctx);
@@ -914,6 +916,13 @@ public:
         }
     }
 
+    void save_identifier_info(expr const & f) {
+        if (!m_noinfo && infom() && pip() && is_constant(f)) {
+            if (auto p = pip()->get_pos_info(f))
+                m_pre_info_data.add_identifier_info(p->first, p->second, const_name(f));
+        }
+    }
+
     void save_synth_data(expr const & e, expr const & r) {
         if (!m_noinfo && infom() && pip() && is_placeholder(e)) {
             if (auto p = pip()->get_pos_info(e)) {