From 76157ba3928d3fd6f0dd99e19985afe1097961d5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Mar 2015 12:16:25 -0700
Subject: [PATCH] fix(frontends/lean/pp): abbreviations with too much arguments

closes #480
---
 src/frontends/lean/pp.cpp         | 6 +++---
 tests/lean/480.hlean              | 2 ++
 tests/lean/480.hlean.expected.out | 1 +
 3 files changed, 6 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/480.hlean
 create mode 100644 tests/lean/480.hlean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index b68c9cf8c..c21b6c7b7 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1073,10 +1073,10 @@ auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn, un
     buffer<level> ls;
     for (unsigned i = 0; i < num_univs; i++)
         ls.push_back(mk_meta_univ(name("?l", i+1)));
-    buffer<expr> args;
+    expr r = mk_constant(abbrev, to_list(ls));
     if (fn)
-        get_app_args(e, args);
-    return pp_child(mk_app(mk_constant(abbrev, to_list(ls)), args), bp, ignore_hide);
+        r = mk_app(r, app_arg(e));
+    return pp_child(r, bp, ignore_hide);
 }
 
 static bool is_pp_atomic(expr const & e) {
diff --git a/tests/lean/480.hlean b/tests/lean/480.hlean
new file mode 100644
index 000000000..fac44c49e
--- /dev/null
+++ b/tests/lean/480.hlean
@@ -0,0 +1,2 @@
+open is_trunc
+check is_contr.mk
diff --git a/tests/lean/480.hlean.expected.out b/tests/lean/480.hlean.expected.out
new file mode 100644
index 000000000..e5f78aefc
--- /dev/null
+++ b/tests/lean/480.hlean.expected.out
@@ -0,0 +1 @@
+is_contr.mk : Π (center : ?A), (Π (a : ?A), center = a) → is_contr ?A