diff --git a/src/kernel/abstract_type_context.h b/src/kernel/abstract_type_context.h
index fd75e3f2e2..c025082574 100644
--- a/src/kernel/abstract_type_context.h
+++ b/src/kernel/abstract_type_context.h
@@ -29,7 +29,7 @@ public:
         \remark Default implementation just invokes \c infer. */
     virtual expr check(expr const & e) { return infer(e); }
     virtual optional<expr> is_stuck(expr const &) { return none_expr(); }
-    virtual name get_local_pp_name(expr const & e) { return local_pp_name(e); }
+    virtual name get_local_pp_name(expr const & e) const { return local_pp_name(e); }
     virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) {
         return mk_local(mk_fresh_name(), pp_name, type, bi);
     }
diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index c7793b1956..d3bf2c0f12 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -279,6 +279,16 @@ class blastenv {
         virtual void commit() override {
             m_stack.pop_back();
         }
+
+        virtual name get_local_pp_name(expr const & e) const override {
+            if (is_href(e)) {
+                state const & s = m_benv.m_curr_state;
+                hypothesis const & h = s.get_hypothesis_decl(e);
+                return h.get_name();
+            } else {
+                return local_pp_name(e);
+            }
+        }
     };
 
     class to_blast_expr_fn : public replace_visitor {
diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 5505f18ffd..555ef7fc1c 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -1136,7 +1136,7 @@ void congruence_closure::propagate_no_confusion_eq(expr const & e1, expr const &
     expr pr         = *get_eqv_proof(get_eq_name(), e1, e2);
     expr H          = s.mk_hypothesis(type, pr);
     lean_trace(name({"cc", "propagation"}),
-               tout() << "no confusion eq: " << ppb(H) << " : " << ppb(infer_type(H)) << "\n";);
+               tout() << "no confusion eq: " << H << " : " << infer_type(H) << "\n";);
 }
 
 /* Remark: If added_prop is not none, then it contains the proposition provided to ::add.
@@ -1284,7 +1284,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
                 }
                 expr H = s.mk_hypothesis(type, pr);
                 lean_trace(name({"cc", "propagation"}),
-                           tout() << ppb(H) << " : " << ppb(infer_type(H)) << "\n";);
+                           tout() << H << " : " << infer_type(H) << "\n";);
             }
         }
     }
@@ -1297,7 +1297,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
     if (R == get_eq_name()) {
         check_new_subsingleton_eq(e1_root, e2_root);
     }
-    lean_trace(name({"cc", "merge"}), tout() << ppb(e1_root) << " [" << R << "] " << ppb(e2_root) << "\n";);
+    lean_trace(name({"cc", "merge"}), tout() << e1_root << " [" << R << "] " << e2_root << "\n";);
     lean_trace(name({"cc", "state"}), trace(););
 }
 
@@ -1913,7 +1913,7 @@ void congruence_closure::trace_eqc(name const & R, expr const & e) const {
     do {
         auto it_n = m_entries.find(eqc_key(R, it));
         if (first) first = false; else out << ", ";
-        out << ppb(it);
+        out << it;
         it = it_n->m_next;
     } while (it != e);
     out << "}";
@@ -1938,13 +1938,13 @@ void congruence_closure::trace_parents() const {
     auto out = tout();
     m_parents.for_each([&](child_key const & k, parent_occ_set const & ps) {
             trace_rel(out, k.m_R);
-            out << ppb(k.m_expr);
+            out << k.m_expr;
             out << ", parents: {";
             bool first = true;
             ps.for_each([&](parent_occ const & o) {
                     if (first) first = false; else out << ", ";
                     trace_rel(out, o.m_R);
-                    out << ppb(o.m_expr);
+                    out << o.m_expr;
                 });
             out << "}\n";
         });
diff --git a/src/library/blast/discr_tree.cpp b/src/library/blast/discr_tree.cpp
index 83df921dca..b21a7769fe 100644
--- a/src/library/blast/discr_tree.cpp
+++ b/src/library/blast/discr_tree.cpp
@@ -399,7 +399,7 @@ void discr_tree::node::trace(optional<edge> const & e, unsigned depth, bool disj
         first = true;
         m_ptr->m_values.for_each([&](expr const & v) {
                 if (first) first = false; else tout() << ", ";
-                tout() << ppb(v);
+                tout() << v;
             });
         tout() << "}";
     }
diff --git a/src/library/blast/forward/ematch.cpp b/src/library/blast/forward/ematch.cpp
index 49e4d6899b..c05e656bd0 100644
--- a/src/library/blast/forward/ematch.cpp
+++ b/src/library/blast/forward/ematch.cpp
@@ -425,8 +425,8 @@ struct ematch_fn {
             expr new_p = m_ctx->instantiate_uvars_mvars(p);
             expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
             expr t_type = m_ctx->infer(t);
-            tout() << "try process_match: " << ppb(p) << " ::= " << ppb(new_p) << " : " << ppb(new_p_type) << " <=?=> "
-            << ppb(t) << " : " << ppb(t_type) << "\n";);
+            tout() << "try process_match: " << p << " ::= " << new_p << " : " << new_p_type << " <=?=> "
+            << t << " : " << t_type << "\n";);
         if (!is_app(p)) {
             bool success = match_leaf(R, p, t);
             return success;
@@ -448,7 +448,7 @@ struct ematch_fn {
                 ok = true;
                 candidates.push_back(it);
             }
-            lean_trace_debug_ematch(tout() << "candidate: " << ppb(it) << "..." << (ok ? "ok" : "skip") << "\n";);
+            lean_trace_debug_ematch(tout() << "candidate: " << it << "..." << (ok ? "ok" : "skip") << "\n";);
             it = m_cc.get_next(R, it);
         } while (it != t);
         if (candidates.empty()) {
@@ -459,7 +459,7 @@ struct ematch_fn {
         for (expr const & c : candidates) {
             state new_state = m_state;
             if (match_args(new_state, R, p_args, c)) {
-                lean_trace_debug_ematch(tout() << "match: " << ppb(c) << "\n";);
+                lean_trace_debug_ematch(tout() << "match: " << c << "\n";);
                 new_states.push_back(new_state);
             }
         }
@@ -468,7 +468,7 @@ struct ematch_fn {
     }
 
     bool process_continue(name const & R, expr const & p) {
-        lean_trace_debug_ematch(tout() << "process_continue: " << ppb(p) << "\n";);
+        lean_trace_debug_ematch(tout() << "process_continue: " << p << "\n";);
         buffer<expr> p_args;
         expr const & f = get_app_args(p, p_args);
         buffer<state> new_states;
@@ -506,8 +506,8 @@ struct ematch_fn {
             expr new_p = m_ctx->instantiate_uvars_mvars(p);
             expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
             expr t_type = m_ctx->infer(t);
-            tout() << "process_matchss: " << ppb(p) << " ::= " << ppb(new_p) << " : " << ppb(new_p_type) << " <=?=> "
-            << ppb(t) << " : " << ppb(t_type) << "\n";);
+            tout() << "process_matchss: " << p << " ::= " << new_p << " : " << new_p_type << " <=?=> "
+            << t << " : " << t_type << "\n";);
         if (!is_metavar(p)) {
             /* If p is not a metavariable we simply ignore it.
                We should improve this case in the future. */
@@ -539,7 +539,7 @@ struct ematch_fn {
         name R; frame_kind kind; expr p, t;
         std::tie(R, kind, p, t) = head(m_state);
         m_state = tail(m_state);
-        // diagnostic(env(), ios()) << ">> " << R << ", " << ppb(p) << " =?= " << ppb(t) << "\n";
+        // diagnostic(env(), ios()) << ">> " << R << ", " << p << " =?= " << t << "\n";
         bool success;
         switch (kind) {
         case DefEqOnly:
@@ -548,8 +548,8 @@ struct ematch_fn {
                 expr new_p = m_ctx->instantiate_uvars_mvars(p);
                 expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
                 expr t_type = m_ctx->infer(t);
-                tout() << "must be def-eq: " << ppb(new_p) << " : " << ppb(new_p_type)
-                << "  =?= " << ppb(t) << " : " << ppb(t_type)
+                tout() << "must be def-eq: " << new_p << " : " << new_p_type
+                << "  =?= " << t << " : " << t_type
                 << " ... " << (success ? "succeeded" : "failed") << "\n";);
             return success;
         case Match:
@@ -560,8 +560,8 @@ struct ematch_fn {
                 expr new_p = m_ctx->instantiate_uvars_mvars(p);
                 expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
                 expr t_type = m_ctx->infer(t);
-                tout() << "must be eqv: " << ppb(new_p) << " : " << ppb(new_p_type) << " =?= "
-                << ppb(t) << " : " << ppb(t_type) << " ... " << (success ? "succeeded" : "failed") << "\n";);
+                tout() << "must be eqv: " << new_p << " : " << new_p_type << " =?= "
+                << t << " : " << t_type << " ... " << (success ? "succeeded" : "failed") << "\n";);
             return success;
         case MatchSS:
             return process_matchss(p, t);
@@ -590,16 +590,16 @@ struct ematch_fn {
         for (expr const & mvar : lemma.m_mvars) {
             if (!m_ctx->get_assignment(mvar)) {
                 if (!head(*it)) {
-                    lean_trace_debug_ematch(tout() << "unassigned argument not inst-implicit: " << ppb(m_ctx->infer(mvar)) << "\n";);
+                    lean_trace_debug_ematch(tout() << "unassigned argument not inst-implicit: " << m_ctx->infer(mvar) << "\n";);
                     return; // fail, argument is not instance implicit
                 }
                 auto new_val = m_ctx->mk_class_instance(m_ctx->infer(mvar));
                 if (!new_val) {
-                    lean_trace_debug_ematch(tout() << "cannot synthesize unassigned inst-implicit argument: " << ppb(m_ctx->infer(mvar)) << "\n";);
+                    lean_trace_debug_ematch(tout() << "cannot synthesize unassigned inst-implicit argument: " << m_ctx->infer(mvar) << "\n";);
                     return; // fail, instance could not be generated
                 }
                 if (!m_ctx->assign(mvar, *new_val)) {
-                    lean_trace_debug_ematch(tout() << "unable to assign inst-implicit argument: " << ppb(*new_val) << " : " << ppb(m_ctx->infer(mvar)) << "\n";);
+                    lean_trace_debug_ematch(tout() << "unable to assign inst-implicit argument: " << *new_val << " : " << m_ctx->infer(mvar) << "\n";);
                     return; // fail, type error
                 }
             }
@@ -613,7 +613,7 @@ struct ematch_fn {
         if (!m_new_instances) {
             trace_action("ematch");
         }
-        lean_trace_ematch(tout() << "instance [" << ppb(lemma.m_expr) << "]: " << ppb(new_inst) << "\n";);
+        lean_trace_ematch(tout() << "instance [" << lemma.m_expr << "]: " << new_inst << "\n";);
         m_new_instances = true;
         expr new_proof = m_ctx->instantiate_uvars_mvars(lemma.m_proof);
         curr_state().mk_hypothesis(new_inst, new_proof);
@@ -643,7 +643,7 @@ struct ematch_fn {
         if (auto s = m_inst_ext.get_apps().find(head_index(f))) {
             s->for_each([&](expr const & t) {
                     if ((m_cc.is_congr_root(R, t) || m_cc.eq_class_heterogeneous(t)) && (!filter || m_cc.get_mt(R, t) == gmt)) {
-                        lean_trace_debug_ematch(tout() << "ematch " << ppb(get_app_fn(lemma.m_proof)) << " [using] " << ppb(t) << "\n";);
+                        lean_trace_debug_ematch(tout() << "ematch " << get_app_fn(lemma.m_proof) << " [using] " << t << "\n";);
                         m_ctx->clear();
                         m_ctx->set_next_uvar_idx(lemma.m_num_uvars);
                         m_ctx->set_next_mvar_idx(lemma.m_num_mvars);
diff --git a/src/library/blast/gexpr.cpp b/src/library/blast/gexpr.cpp
index 584809c9d6..1c2101d837 100644
--- a/src/library/blast/gexpr.cpp
+++ b/src/library/blast/gexpr.cpp
@@ -37,7 +37,7 @@ std::ostream & operator<<(std::ostream & out, gexpr const & ge) {
 }
 
 io_state_stream const & operator<<(io_state_stream const & out, gexpr const & ge) {
-    out << ppb(ge.m_expr);
+    out << ge.m_expr;
     if (ge.is_universe_polymorphic()) out << " (poly)";
     return out;
 }
diff --git a/src/library/blast/recursor/recursor_strategy.cpp b/src/library/blast/recursor/recursor_strategy.cpp
index c440877f9e..115c925227 100644
--- a/src/library/blast/recursor/recursor_strategy.cpp
+++ b/src/library/blast/recursor/recursor_strategy.cpp
@@ -95,7 +95,7 @@ public:
             action_result r     = try_hypothesis(hidx);
             if (!failed(r)) {
                 lean_trace_search(tout() << "next of choice #" << m_choice_idx
-                                  << ", recurse " << ppb(mk_href(hidx)) << "\n";);
+                                  << ", recurse " << mk_href(hidx) << "\n";);
                 return r;
             }
         }
@@ -121,9 +121,9 @@ action_result rec_action(rec_candidate_selector const & selector) {
                 // create choice point
                 unsigned cidx = mk_choice_point_idx();
                 push_choice_point(choice_point(new rec_choice_point_cell(s, hidx_list, cidx)));
-                lean_trace_search(tout() << "recurse " << ppb(mk_href(hidx)) << " (choice #" << cidx << ")\n";);
+                lean_trace_search(tout() << "recurse " << mk_href(hidx) << " (choice #" << cidx << ")\n";);
             } else {
-                lean_trace_search(tout() << "recurse " << ppb(mk_href(hidx)) << "\n";);
+                lean_trace_search(tout() << "recurse " << mk_href(hidx) << "\n";);
             }
             return r;
         }
diff --git a/src/library/blast/simplifier/simplifier.cpp b/src/library/blast/simplifier/simplifier.cpp
index f92715df87..b5e2747957 100644
--- a/src/library/blast/simplifier/simplifier.cpp
+++ b/src/library/blast/simplifier/simplifier.cpp
@@ -384,7 +384,7 @@ result simplifier::simplify(expr const & e, bool is_root) {
     check_system("simplifier");
     m_num_steps++;
     lean_trace_inc_depth("simplifier");
-    lean_trace_d("simplifier", tout() << m_rel << ": " << ppb(e) << "\n";);
+    lean_trace_d("simplifier", tout() << m_rel << ": " << e << "\n";);
 
     if (m_num_steps > m_max_steps)
         throw blast_exception("simplifier failed, maximum number of steps exceeded", e);
@@ -627,7 +627,7 @@ result simplifier::rewrite(expr const & e, simp_lemma const & sr) {
                expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
                expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
                tout() << "(" << sr.get_id() << ") "
-               << "[" << ppb(new_lhs) << " --> " << ppb(new_rhs) << "]\n";);
+               << "[" << new_lhs << " --> " << new_rhs << "]\n";);
 
     if (!instantiate_emetas(tmp_tctx, sr.get_num_emeta(), sr.get_emetas(), sr.get_instances())) return result(e);
 
@@ -720,7 +720,7 @@ result simplifier::try_congr(expr const & e, user_congr_lemma const & cr) {
                expr new_rhs = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs());
                diagnostic(env(), ios(), get_type_context())
                << "(" << cr.get_id() << ") "
-               << "[" << ppb(new_lhs) << " =?= " << ppb(new_rhs) << "]\n";);
+               << "[" << new_lhs << " =?= " << new_rhs << "]\n";);
 
     /* First, iterate over the congruence hypotheses */
     bool failed = false;
@@ -787,13 +787,13 @@ bool simplifier::instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned
                 if (auto v = tmp_tctx->mk_class_instance(m_type)) {
                     if (!tmp_tctx->assign(m, *v)) {
                         lean_trace(name({"simplifier", "failure"}),
-                                   tout() << "unable to assign instance for: " << ppb(m_type) << "\n";);
+                                   tout() << "unable to assign instance for: " << m_type << "\n";);
                         failed = true;
                         return;
                     }
                 } else {
                     lean_trace(name({"simplifier", "failure"}),
-                               tout() << "unable to synthesize instance for: " << ppb(m_type) << "\n";);
+                               tout() << "unable to synthesize instance for: " << m_type << "\n";);
                     failed = true;
                     return;
                 }
@@ -809,7 +809,7 @@ bool simplifier::instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned
             }
 
             lean_trace(name({"simplifier", "failure"}),
-                       tout() << "failed to assign: " << m << " : " << ppb(m_type) << "\n";);
+                       tout() << "failed to assign: " << m << " : " << m_type << "\n";);
 
             failed = true;
             return;
@@ -1081,7 +1081,7 @@ result simplifier::fuse(expr const & e) {
                         get_simp_lemmas(g_ac_key));
 
     if (!pf_1_3) {
-        diagnostic(env(), ios(), get_type_context()) << ppb(e) << "\n\n =?=\n\n" << ppb(e_grp) << "\n";
+        diagnostic(env(), ios(), get_type_context()) << e << "\n\n =?=\n\n" << e_grp << "\n";
         throw blast_exception("Failed to prove (1) == (3) during fusion", e);
     }
 
@@ -1090,7 +1090,7 @@ result simplifier::fuse(expr const & e) {
                         get_simp_lemmas(g_som_key));
 
     if (!pf_4_5) {
-        diagnostic(env(), ios(), get_type_context()) << ppb(e_grp_ls) << "\n\n =?=\n\n" << ppb(e_fused_ls) << "\n";
+        diagnostic(env(), ios(), get_type_context()) << e_grp_ls << "\n\n =?=\n\n" << e_fused_ls << "\n";
         throw blast_exception("Failed to prove (4) == (5) during fusion", e);
     }
 
diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp
index f4d868e309..b0a93cdf41 100644
--- a/src/library/blast/state.cpp
+++ b/src/library/blast/state.cpp
@@ -886,7 +886,7 @@ optional<unsigned> state::select_hypothesis_to_activate() {
 void state::activate_hypothesis(hypothesis_idx hidx) {
     lean_trace_search(
         hypothesis const & h = get_hypothesis_decl(hidx);
-        tout() << "activate " << h.get_name() << " : " << ppb(h.get_type()) << "\n";);
+        tout() << "activate " << h.get_name() << " : " << h.get_type() << "\n";);
     lean_assert(!get_hypothesis_decl(hidx).is_dead());
     m_branch.m_active.insert(hidx);
     update_indices(hidx);
diff --git a/src/library/blast/trace.cpp b/src/library/blast/trace.cpp
index e1969cdb1d..6fca1fa92e 100644
--- a/src/library/blast/trace.cpp
+++ b/src/library/blast/trace.cpp
@@ -19,7 +19,7 @@ MK_THREAD_LOCAL_GET_DEF(expr, get_last_target);
 void trace_target() {
     if (lean_is_trace_enabled(name({"blast", "search"})) &&
         curr_state().get_target() != get_last_target()) {
-        lean_trace_search(tout() << "target " << ppb(curr_state().get_target()) << "\n";);
+        lean_trace_search(tout() << "target " << curr_state().get_target() << "\n";);
         get_last_target() = curr_state().get_target();
     }
 }
@@ -83,14 +83,8 @@ void trace_curr_state_if(action_result r) {
         trace_curr_state();
 }
 
-io_state_stream const & operator<<(io_state_stream const & out, ppb const & e) {
-    expr tmp = curr_state().to_kernel_expr(e.m_expr);
-    out << tmp;
-    return out;
-}
-
 io_state_stream const & operator<<(io_state_stream const & out, hypothesis const & h) {
-    out << ppb(h.get_self());
+    out << h.get_self();
     return out;
 }
 }}
diff --git a/src/library/blast/trace.h b/src/library/blast/trace.h
index 6c9e6fc188..616673d1de 100644
--- a/src/library/blast/trace.h
+++ b/src/library/blast/trace.h
@@ -24,14 +24,5 @@ void trace_curr_state_if(action_result r);
 #define lean_trace_search(Code) lean_trace(name({"blast", "search"}), Code)
 #define lean_trace_deadend(Code) lean_trace(name({"blast", "deadend"}), Code)
 
-/** \brief Helper class for pretty printing blast expressions.
-    It uses state::to_kernel_expr to export a blast expression
-    into an expression that can be processed by the pretty printer */
-struct ppb {
-    expr m_expr;
-    explicit ppb(expr const & e):m_expr(e) {}
-};
-
-io_state_stream const & operator<<(io_state_stream const & out, ppb const & e);
 io_state_stream const & operator<<(io_state_stream const & out, hypothesis const & h);
 }}
diff --git a/src/library/blast/unit/unit_propagate.cpp b/src/library/blast/unit/unit_propagate.cpp
index 6521c23f30..345ca68d6b 100644
--- a/src/library/blast/unit/unit_propagate.cpp
+++ b/src/library/blast/unit/unit_propagate.cpp
@@ -294,7 +294,7 @@ static action_result unit_lemma(hypothesis_idx hidx, expr const & _type, expr co
     }
 
     curr_state().mk_hypothesis(final_type, final_proof);
-    lean_trace_unit_propagate(tout() << ppb(final_type) << "\n";);
+    lean_trace_unit_propagate(tout() << final_type << "\n";);
     return action_result::new_branch();
 }
 
@@ -316,7 +316,7 @@ static action_result unit_dep_lemma(hypothesis_idx hidx, expr type, expr proof)
     if (propagated) {
         curr_state().del_hypothesis(hidx);
         curr_state().mk_hypothesis(type, proof);
-        lean_trace_unit_propagate(tout() << ppb(type) << "\n";);
+        lean_trace_unit_propagate(tout() << type << "\n";);
         return action_result::new_branch();
     }
     lean_assert(is_pi(type));
@@ -351,7 +351,7 @@ static action_result unit_fact(expr const & type) {
 action_result unit_propagate(unsigned hidx) {
     hypothesis const & h = curr_state().get_hypothesis_decl(hidx);
     expr type = whnf(h.get_type());
-    lean_trace_debug_unit_propagate(tout() << ppb(type) << "\n";);
+    lean_trace_debug_unit_propagate(tout() << type << "\n";);
     if (is_lemma(type)) return unit_lemma(hidx, type, h.get_self());
     else if (is_dep_lemma(type)) return unit_dep_lemma(hidx, type, h.get_self());
     else if (is_fact(type)) return unit_fact(type);