diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 12dda551a8..8784531c2a 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -152,7 +152,7 @@ def to_level : syntax → elaborator_m level
   st ← get,
   match fn.kind with
   | some level.leading := (match view level.leading stx, args with
-    | level.leading.view.hole _, [] := pure $ level.mvar "u"  -- TODO(Sebastian): name?
+    | level.leading.view.hole _, [] := pure $ level.mvar name.anonymous
     | level.leading.view.lit lit, [] := pure $ level.of_nat lit.to_nat
     | level.leading.view.var id, [] := let id := mangle_ident id in (match st.local_state.univs.find id with
       | some _ := pure $ level.param id
@@ -204,7 +204,7 @@ def to_pexpr : syntax → elaborator_m expr
     let v := view anonymous_constructor stx,
     p ← to_pexpr $ mk_app (review hole {}) (v.args.map sep_by.elem.view.item),
     pure $ expr.mk_annotation `anonymous_constructor p
-  | @hole := pure $ expr.const "_" []  -- TODO
+  | @hole := pure $ expr.mvar name.anonymous dummy
   | @«have» := do
     let v := view «have» stx,
     let id := (mangle_ident <$> opt_ident.view.id <$> v.id).get_or_else `this,
diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp
index 0898a8083c..72f7e96018 100644
--- a/src/library/placeholder.cpp
+++ b/src/library/placeholder.cpp
@@ -20,29 +20,19 @@ void finalize_placeholder() {
     delete g_placeholder_name;
 }
 
-LEAN_THREAD_VALUE(unsigned, g_placeholder_id, 0);
-static unsigned next_placeholder_id() {
-    unsigned r = g_placeholder_id;
-    g_placeholder_id++;
-    return r;
-}
-level mk_level_placeholder() { return mk_univ_param(name(*g_placeholder_name, next_placeholder_id())); }
+level mk_level_placeholder() { return mk_univ_mvar(name()); }
 
 expr mk_expr_placeholder() {
-    name n(*g_placeholder_name, next_placeholder_id());
-    return mk_constant(n);
+    return mk_mvar(name(), mk_Prop());
 }
 static bool is_placeholder(name const & n) {
-    if (n.is_atomic())
-        return false;
-    name const & p = n.get_prefix();
-    return p == *g_placeholder_name;
+    return n.is_anonymous();
 }
-bool is_placeholder(level const & e) { return is_param(e) && is_placeholder(param_id(e)); }
+bool is_placeholder(level const & e) { return is_mvar(e) && is_placeholder(mvar_id(e)); }
 
 bool is_placeholder(expr const & e) {
     expr e2 = unwrap_pos(e);
-    return is_constant(e2) && is_placeholder(const_name(e2));
+    return is_mvar(e2) && is_placeholder(mvar_name(e2));
 }
 
 bool has_placeholder(level const & l) {