From 288831dc66b6c2faeaa577bb3684a16c0284ed85 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Aug 2014 15:07:01 -0700 Subject: [PATCH] fix(kernel/formatter): fixes #21 Signed-off-by: Leonardo de Moura --- src/kernel/formatter.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) 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 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); }