diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 759fd0954b..e6f29a3da6 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -331,10 +331,10 @@ public:
     expr visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs) {
         lean_assert(is_proof_qed_annotation(e));
         pair<expr, constraint_seq> ecs = visit(get_annotation_arg(e));
-        pair<expr, constraint> mc = mk_proof_qed_elaborator(env(), m_full_context, ecs.first, t, ecs.second,
-                                                            m_unifier_config, m_relax_main_opaque);
-        cs += mc.second;
-        return mc.first;
+        expr m                         = m_full_context.mk_meta(t, e.get_tag());
+        constraint c                   = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second, m_unifier_config, m_relax_main_opaque);
+        cs += c;
+        return m;
     }
 
     static bool is_implicit_pi(expr const & e) {
diff --git a/src/frontends/lean/proof_qed_elaborator.cpp b/src/frontends/lean/proof_qed_elaborator.cpp
index 3e6e7f08b1..7d9fcf2c27 100644
--- a/src/frontends/lean/proof_qed_elaborator.cpp
+++ b/src/frontends/lean/proof_qed_elaborator.cpp
@@ -8,9 +8,10 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/metavar_closure.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/local_context.h"
-
 namespace lean {
+/** \brief Create a "choice" constraint that postpone the
+    solving the constraints <tt>(cs union (m =?= e))</tt>.
+*/
 constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e,
                               constraint_seq const & cs, unifier_config const & cfg, bool relax) {
     justification j         = mk_failed_to_synthesize_jst(env, m);
@@ -47,16 +48,4 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons
     bool owner = false;
     return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax);
 }
-
-/** \brief Create a metavariable m, and attach "choice" constraint that postpone the
-    solving the constraints <tt>(cs union m =?= e)</tt>.
-*/
-pair<expr, constraint> mk_proof_qed_elaborator(
-    environment const & env, local_context & ctx,
-    expr const & e, optional<expr> const & type, constraint_seq const & cs,
-    unifier_config const & cfg, bool relax) {
-    expr m       = ctx.mk_meta(type, e.get_tag());
-    constraint c = mk_proof_qed_cnstr(env, m, e, cs, cfg, relax);
-    return mk_pair(m, c);
-}
 }
diff --git a/src/frontends/lean/proof_qed_elaborator.h b/src/frontends/lean/proof_qed_elaborator.h
index e426d9c8aa..c9d759f26b 100644
--- a/src/frontends/lean/proof_qed_elaborator.h
+++ b/src/frontends/lean/proof_qed_elaborator.h
@@ -8,10 +8,9 @@ Author: Leonardo de Moura
 #include "library/unifier.h"
 
 namespace lean {
-/** \brief Create a metavariable m, and attach "choice" constraint that postpone the
-    solving the constraints <tt>(cs union m =?= e)</tt>.
+/** \brief Create a "choice" constraint that postpone the
+    solving the constraints <tt>(cs union (m =?= e))</tt>.
 */
-pair<expr, constraint> mk_proof_qed_elaborator(environment const & env, local_context & ctx,
-                                               expr const & e, optional<expr> const & type, constraint_seq const & cs,
-                                               unifier_config const & cfg, bool relax);
+constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e,
+                              constraint_seq const & cs, unifier_config const & cfg, bool relax);
 }