diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 0377e6a893..c2a9c63177 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -343,7 +343,6 @@ void pretty_fn::set_options_core(options const & _o) {
     m_preterm           = get_pp_preterm(o);
     m_binder_types      = get_pp_binder_types(o);
     m_hide_comp_irrel   = get_pp_hide_comp_irrel(o);
-    m_use_holes         = get_pp_use_holes(o);
     m_annotations       = get_pp_annotations(o);
     m_hide_full_terms   = get_formatter_hide_full_terms(o);
     m_num_nat_coe       = m_numerals;
@@ -751,12 +750,8 @@ auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ
     }
 }
 
-static format pp_hole() { return format("{! !}"); }
-
 auto pretty_fn::pp_meta(expr const & e) -> result {
-    if (m_use_holes) {
-        return pp_hole();
-    } else if (mlocal_name(e) != mlocal_pp_name(e)) {
+    if (mlocal_name(e) != mlocal_pp_name(e)) {
         return result(format(mlocal_pp_name(e)));
     } else if (is_idx_metavar(e)) {
         return result(format((sstream() << "?x_" << to_meta_idx(e)).str()));
@@ -1171,15 +1166,9 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
         else
             return pp(get_annotation_arg(e));
     } else if (is_synthetic_sorry(e)) {
-        if (m_use_holes)
-            return pp_hole();
-        else
-            return m_unicode ? format("⁇") : format("??");
+        return m_unicode ? format("⁇") : format("??");
     } else if (is_sorry(e)) {
-        if (m_use_holes)
-            return pp_hole();
-        else
-            return format("sorry");
+        return format("sorry");
     } else {
         return pp_macro_default(e);
     }
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index 9ecf8ed265..b7b0363710 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -86,7 +86,6 @@ private:
     bool                    m_structure_instances;
     bool                    m_structure_instances_qualifier;
     bool                    m_structure_projections;
-    bool                    m_use_holes;
     bool                    m_annotations;
 
     name mk_metavar_name(name const & m, optional<name> const & prefix = optional<name>());
diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp
index 92f0547935..64d448b7d1 100644
--- a/src/library/pp_options.cpp
+++ b/src/library/pp_options.cpp
@@ -108,10 +108,6 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_PP_INSTANTIATE_MVARS true
 #endif
 
-#ifndef LEAN_DEFAULT_PP_USE_HOLES
-#define LEAN_DEFAULT_PP_USE_HOLES false
-#endif
-
 #ifndef LEAN_DEFAULT_PP_ANNOTATIONS
 #define LEAN_DEFAULT_PP_ANNOTATIONS false
 #endif
@@ -141,7 +137,6 @@ static name * g_pp_structure_instances = nullptr;
 static name * g_pp_structure_instances_qualifier = nullptr;
 static name * g_pp_structure_projections    = nullptr;
 static name * g_pp_instantiate_mvars = nullptr;
-static name * g_pp_use_holes         = nullptr;
 static name * g_pp_annotations       = nullptr;
 static name * g_pp_all               = nullptr;
 static list<options> * g_distinguishing_pp_options = nullptr;
@@ -172,7 +167,6 @@ void initialize_pp_options() {
     g_pp_structure_instances_qualifier = new name{"pp", "structure_instances_qualifier"};
     g_pp_structure_projections = new name{"pp", "structure_projections"};
     g_pp_instantiate_mvars = new name{"pp", "instantiate_mvars"};
-    g_pp_use_holes         = new name{"pp", "use_holes"};
     g_pp_annotations       = new name{"pp", "annotations"};
 
     register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
@@ -231,8 +225,6 @@ void initialize_pp_options() {
                          "and disable beta reduction and notation during pretty printing");
     register_bool_option(*g_pp_instantiate_mvars, LEAN_DEFAULT_PP_INSTANTIATE_MVARS,
                          "(pretty printer) instantiate assigned metavariables before pretty printing terms and goals");
-    register_bool_option(*g_pp_use_holes, LEAN_DEFAULT_PP_USE_HOLES,
-                         "(pretty printer) use holes '{! !}' when pretty printing metavariables and `sorry`");
     register_bool_option(*g_pp_annotations, LEAN_DEFAULT_PP_ANNOTATIONS,
                          "(pretty printer) display internal annotations (for debugging purposes only)");
 
@@ -278,7 +270,6 @@ void finalize_pp_options() {
     delete g_pp_structure_projections;
     delete g_pp_all;
     delete g_pp_instantiate_mvars;
-    delete g_pp_use_holes;
     delete g_pp_annotations;
     delete g_distinguishing_pp_options;
 }
@@ -296,7 +287,6 @@ name const & get_pp_beta_name() { return *g_pp_beta; }
 name const & get_pp_preterm_name() { return *g_pp_preterm; }
 name const & get_pp_numerals_name() { return *g_pp_numerals; }
 name const & get_pp_strings_name() { return *g_pp_strings; }
-name const & get_pp_use_holes_name() { return *g_pp_use_holes; }
 name const & get_pp_binder_types_name() { return *g_pp_binder_types; }
 
 unsigned get_pp_max_depth(options const & opts)         { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
@@ -323,7 +313,6 @@ bool     get_pp_structure_instances(options const & opts) { return opts.get_bool
 bool     get_pp_structure_instances_qualifier(options const & opts) { return opts.get_bool(*g_pp_structure_instances_qualifier, LEAN_DEFAULT_PP_STRUCTURE_INSTANCES_QUALIFIER); }
 bool     get_pp_structure_projections(options const & opts) { return opts.get_bool(*g_pp_structure_projections, LEAN_DEFAULT_PP_STRUCTURE_PROJECTIONS); }
 bool     get_pp_instantiate_mvars(options const & o)    { return o.get_bool(*g_pp_instantiate_mvars, LEAN_DEFAULT_PP_INSTANTIATE_MVARS); }
-bool     get_pp_use_holes(options const & o)            { return o.get_bool(*g_pp_use_holes, LEAN_DEFAULT_PP_USE_HOLES); }
 bool     get_pp_annotations(options const & o)          { return o.get_bool(*g_pp_annotations, LEAN_DEFAULT_PP_ANNOTATIONS); }
 bool     get_pp_all(options const & opts)               { return opts.get_bool(*g_pp_all, LEAN_DEFAULT_PP_ALL); }
 }
diff --git a/src/library/pp_options.h b/src/library/pp_options.h
index 2e34296246..371b5c366c 100644
--- a/src/library/pp_options.h
+++ b/src/library/pp_options.h
@@ -21,7 +21,6 @@ name const & get_pp_preterm_name();
 name const & get_pp_numerals_name();
 name const & get_pp_strings_name();
 name const & get_pp_binder_types_name();
-name const & get_pp_use_holes_name();
 
 unsigned get_pp_max_depth(options const & opts);
 unsigned get_pp_max_steps(options const & opts);
@@ -47,7 +46,6 @@ bool     get_pp_structure_instances(options const & opts);
 bool     get_pp_structure_instances_qualifier(options const & opts);
 bool     get_pp_structure_projections(options const & opts);
 bool     get_pp_instantiate_mvars(options const & o);
-bool     get_pp_use_holes(options const & o);
 bool     get_pp_annotations(options const & o);
 bool     get_pp_all(options const & opts);