diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp
index d377b48fc..e1fdc6e32 100644
--- a/src/kernel/formatter.cpp
+++ b/src/kernel/formatter.cpp
@@ -31,9 +31,19 @@ name pick_unused_name(expr const & t, name const & s) {
     return r;
 }
 
+bool is_internal_name(name n) {
+    while (!n.is_atomic())
+        n = n.get_prefix();
+    return n.is_numeral();
+}
+
+static name g_x("x");
 std::pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
     lean_assert(is_binding(b));
-    name n = pick_unused_name(binding_body(b), binding_name(b));
+    name n = binding_name(b);
+    if (is_internal_name(n))
+        n = g_x;
+    n = pick_unused_name(binding_body(b), n);
     expr c = mk_local(n, preserve_type ? binding_domain(b) : expr());
     return mk_pair(instantiate(binding_body(b), c), c);
 }