From 4a75e2d965095056c81e6901ea3d1d62204c6c37 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Sep 2013 17:51:56 -0700 Subject: [PATCH] Fix bug when pretty printing function applications where the head is a meta-variable. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_pp.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp index 7aaf7bccc..841c54157 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -648,8 +648,8 @@ class pp_fn { } else { // standard function application expr const & f = app.get_function(); - result p = is_constant(f) ? mk_result(format(const_name(f)),1) : pp_child(f, depth); - bool simple = is_constant(f) && const_name(f).size() <= m_indent + 4; + result p = is_constant(f) && !is_metavar(f) ? mk_result(format(const_name(f)),1) : pp_child(f, depth); + bool simple = is_constant(f) && !is_metavar(f) && const_name(f).size() <= m_indent + 4; unsigned indent = simple ? const_name(f).size()+1 : m_indent; format r_format = p.first; unsigned r_weight = p.second;