diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp
index dcebfa82f0..7c6e62e232 100644
--- a/src/library/metavar_context.cpp
+++ b/src/library/metavar_context.cpp
@@ -13,12 +13,15 @@ namespace lean {
 static name *       g_meta_prefix;
 static expr *       g_dummy_type;
 
-name mk_meta_decl_name() {
+static name mk_meta_decl_name() {
     return mk_tagged_fresh_name(*g_meta_prefix);
 }
 
-expr mk_meta_ref(name const & n) {
-    return mk_metavar(n, *g_dummy_type);
+static expr mk_meta_ref(name const & n, optional<name> const & pp_n) {
+    if (pp_n)
+        return mk_metavar(n, *pp_n, *g_dummy_type);
+    else
+        return mk_metavar(n, *g_dummy_type);
 }
 
 bool is_metavar_decl_ref(level const & u) {
@@ -46,10 +49,10 @@ level metavar_context::mk_univ_metavar_decl() {
     return mk_meta_univ(mk_meta_decl_name());
 }
 
-expr metavar_context::mk_metavar_decl(local_context const & ctx, expr const & type) {
+expr metavar_context::mk_metavar_decl(optional<name> const & pp_n, local_context const & ctx, expr const & type) {
     name n = mk_meta_decl_name();
     m_decls.insert(n, metavar_decl(ctx, head_beta_reduce(type)));
-    return mk_meta_ref(n);
+    return mk_meta_ref(n, pp_n);
 }
 
 optional<metavar_decl> metavar_context::find_metavar_decl(expr const & e) const {
diff --git a/src/library/metavar_context.h b/src/library/metavar_context.h
index 6aaa868730..5e8bd6bc99 100644
--- a/src/library/metavar_context.h
+++ b/src/library/metavar_context.h
@@ -31,9 +31,15 @@ class metavar_context {
     name_map<expr>         m_eassignment;
     struct interface_impl;
     friend struct interface_impl;
+    expr mk_metavar_decl(optional<name> const & pp_n, local_context const & ctx, expr const & type);
 public:
     level mk_univ_metavar_decl();
-    expr mk_metavar_decl(local_context const & ctx, expr const & type);
+    expr mk_metavar_decl(local_context const & ctx, expr const & type) {
+        return mk_metavar_decl(optional<name>(), ctx, type);
+    }
+    expr mk_metavar_decl(name const & pp_name, local_context const & ctx, expr const & type) {
+        return mk_metavar_decl(optional<name>(pp_name), ctx, type);
+    }
 
     optional<metavar_decl> find_metavar_decl(expr const & mvar) const;