From 20ab59c740ede74d0884a3197c17ffde44fc7878 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Oct 2014 14:14:08 -0700
Subject: [PATCH] fix(frontends/lean/pp): avoid unnecessary parentheses when
 pretty printing delimited notation

---
 src/frontends/lean/pp.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 4b74868ef..8c5cf6ce4 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -737,7 +737,7 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
             case notation::action_kind::Skip:
                 curr = format(tk);
                 if (last)
-                    last_rbp = get_some_precedence(m_token_table, tk);
+                    last_rbp = max_bp();
                 break;
             case notation::action_kind::Expr:
                 if (args.empty() || !args.back()) {
@@ -873,8 +873,9 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
             }
             extra_space = add_extra_space(tk);
         }
-        unsigned first_lbp = token_lbp;
+        unsigned first_lbp = max_bp();
         if (!entry.is_nud()) {
+            first_lbp = token_lbp;
             lean_assert(!last);
             if (args.size() != 1 || !args.back())
                 return optional<result>();