diff --git a/src/kernel/printer.cpp b/src/kernel/printer.cpp
index 34f9d74557..97ef93b6dc 100644
--- a/src/kernel/printer.cpp
+++ b/src/kernel/printer.cpp
@@ -102,7 +102,7 @@ struct print_expr_fn {
         case expr_kind::Var: {
             auto e = find(c, var_idx(a));
             if (e)
-                out() << e->get_name();
+                out() << e->get_name() << "#" << var_idx(a);
             else
                 out() << "#" << var_idx(a);
             break;
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index acd0afbb12..c9693b0d66 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -315,11 +315,11 @@ static void tst16() {
     expr a = Const("a");
     expr x = Var(0);
     ctx = extend(ctx, "x", Const("N"));
-    check_justification_msg(mk_function_expected_justification(ctx, f(a, x)), "Function expected at\n  f a x");
-    check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x");
-    check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n  Pi a : N, (x a)");
-    check_justification_msg(mk_app_type_match_justification(ctx, f(a, x), 1), "Type of argument 1 must be convertible to the expected type in the application of\n  f\nwith arguments:\n  a\n  x");
-    check_justification_msg(mk_max_type_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x");
+    check_justification_msg(mk_function_expected_justification(ctx, f(a, x)), "Function expected at\n  f a x#0");
+    check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x#1");
+    check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n  Pi a : N, (x#1 a#0)");
+    check_justification_msg(mk_app_type_match_justification(ctx, f(a, x), 1), "Type of argument 1 must be convertible to the expected type in the application of\n  f\nwith arguments:\n  a\n  x#0");
+    check_justification_msg(mk_max_type_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x#1");
     check_justification_msg(mk_def_type_match_justification(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type.");
 }
 
diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp
index 1fe7e9552f..6742c1284a 100644
--- a/src/tests/library/formatter.cpp
+++ b/src/tests/library/formatter.cpp
@@ -30,15 +30,15 @@ static void tst1() {
     expr y  = Const("y");
     expr N  = Const("N");
     expr F  = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(Eq(x, f(y, a)))));
-    check(fmt(F), "fun x : (Pi x : N, (x -> x)), (let y := f a in (f (x == (f y a))))");
+    check(fmt(F), "fun x : (Pi x : N, (x#0 -> x#1)), (let y := f a in (f (x#1 == (f y#0 a))))");
     check(fmt(env->get_object("N")), "Variable N : Type");
     context ctx;
     ctx = extend(ctx, "x", f(a));
     ctx = extend(ctx, "y", f(Var(0), N >> N));
     ctx = extend(ctx, "z", N, Eq(Var(0), Var(1)));
-    check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y == x]");
-    check(fmt(ctx, f(Var(0), Var(2))), "f z x");
-    check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y == x] |- f z x");
+    check(fmt(ctx), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1]");
+    check(fmt(ctx, f(Var(0), Var(2))), "f z#0 x#2");
+    check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1] |- f z#0 x#2");
 }
 
 int main() {