diff --git a/src/library/util.cpp b/src/library/util.cpp
index e267993fa..164812520 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -822,9 +822,11 @@ justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr con
         });
 }
 
-format format_goal(formatter const & fmt, buffer<expr> const & hyps, expr const & conclusion, substitution const & s) {
+format format_goal(formatter const & _fmt, buffer<expr> const & hyps, expr const & conclusion, substitution const & s) {
     substitution tmp_subst(s);
-    options const & opts = fmt.get_options();
+    options opts     = _fmt.get_options();
+    opts             = opts.update_if_undef(get_pp_purify_locals_name(), false);
+    formatter fmt    = _fmt.update_options(opts);
     unsigned indent  = get_pp_indent(opts);
     bool unicode     = get_pp_unicode(opts);
     bool compact     = get_pp_compact_goals(opts);
diff --git a/tests/lean/assert_fail.lean.expected.out b/tests/lean/assert_fail.lean.expected.out
index 07deb34a6..a92e471ca 100644
--- a/tests/lean/assert_fail.lean.expected.out
+++ b/tests/lean/assert_fail.lean.expected.out
@@ -4,7 +4,7 @@ H : b ∧ a
 ⊢ a
 
 a b : Prop,
-H_1 : b ∧ a,
+H : b ∧ a,
 H : a
 ⊢ a ∧ b
 assert_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
diff --git a/tests/lean/assert_tac2.lean.expected.out b/tests/lean/assert_tac2.lean.expected.out
index c821e07dd..9cf6e7403 100644
--- a/tests/lean/assert_tac2.lean.expected.out
+++ b/tests/lean/assert_tac2.lean.expected.out
@@ -2,7 +2,7 @@ assert_tac2.lean:11:2: proof state
 a b c : ℕ,
 h1 : a = 2,
 h2 : b = 3,
-H_2 : a + b = 2 + b,
-H_1 : a + b = 2 + 3,
+H : a + b = 2 + b,
+H : a + b = 2 + 3,
 H : a + b = 5
 ⊢ 5 + c = c + 5