diff --git a/tests/lean/ctx_error_msgs.lean b/tests/lean/ctx_error_msgs.lean
index e92153b0e0..aef8c9811e 100644
--- a/tests/lean/ctx_error_msgs.lean
+++ b/tests/lean/ctx_error_msgs.lean
@@ -1,7 +1,5 @@
 open tactic
 
-set_option pp.locals_full_names true
-
 example (f : nat) (a : nat) : true :=
 by do
    f ← get_local `f,
diff --git a/tests/lean/ctx_error_msgs.lean.expected.out b/tests/lean/ctx_error_msgs.lean.expected.out
index 86624b7b43..cdd24d50fe 100644
--- a/tests/lean/ctx_error_msgs.lean.expected.out
+++ b/tests/lean/ctx_error_msgs.lean.expected.out
@@ -1,22 +1,22 @@
-ctx_error_msgs.lean:6:0: error: infer type failed, function expected at
-  <f.1.16.0> <a.1.16.1>
+ctx_error_msgs.lean:4:0: error: infer type failed, function expected at
+  f a
 term
-  <f.1.16.0>
+  f
 has type
   ℕ
 state:
 f a : ℕ
 ⊢ true
-ctx_error_msgs.lean:13:0: error: infer type failed, unknown variable
-  <a.1.16.324>
+ctx_error_msgs.lean:11:0: error: infer type failed, unknown variable
+  a
 state:
 ⊢ true
-ctx_error_msgs.lean:20:0: error: infer type failed, incorrect number of universe levels
+ctx_error_msgs.lean:18:0: error: infer type failed, incorrect number of universe levels
   eq
 state:
 a : ℕ
 ⊢ true
-ctx_error_msgs.lean:25:0: error: infer type failed, incorrect number of universe levels
+ctx_error_msgs.lean:23:0: error: infer type failed, incorrect number of universe levels
   eq.{0 0}
 state:
 a : ℕ