diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 39dba7c28..a03eb9c72 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -210,7 +210,7 @@ static expr parse_proof(parser & p, expr const & prop) {
             --i;
             expr l = locals[i];
             pr = p.save_pos(Fun(l, pr), using_pos);
-            pr = p.save_pos(pr(l), using_pos);
+            pr = p.save_pos(mk_app(pr, l), using_pos);
         }
         return pr;
     } else {
@@ -256,7 +256,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
         auto proof_pos = p.pos();
         proof = parse_proof(p, prop);
         proof = p.save_pos(Fun(*prev_local, proof), proof_pos);
-        proof = p.save_pos(proof(*prev_local), proof_pos);
+        proof = p.save_pos(mk_app(proof, *prev_local), proof_pos);
     } else {
         proof = parse_proof(p, prop);
     }
@@ -327,12 +327,12 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
         expr a      = ps[i];
         expr H_aux  = mk_local(p.mk_fresh_name(), H_name.append_after(i), mk_expr_placeholder(), mk_contextual_info(false));
         expr  H2    = Fun({a, H}, b);
-        b = mk_constant(*g_exists_elim)(H_aux, H2);
+        b = mk_app(mk_constant(*g_exists_elim), H_aux, H2);
         H = H_aux;
     }
     expr a  = ps[0];
     expr H2 = Fun({a, H}, b);
-    expr r  = mk_constant(*g_exists_elim)(H1, H2);
+    expr r  = mk_app(mk_constant(*g_exists_elim), H1, H2);
     return p.rec_save_pos(r, pos);
 }
 
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 177fb20a3..d8bf50b06 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -144,21 +144,6 @@ public:
     friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g);
 
     friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
-    // Overloaded operator() can be used to create applications
-    expr operator()(expr const & a1, tag g = nulltag) const;
-    expr operator()(expr const & a1, expr const & a2, tag g = nulltag) const;
-    expr operator()(expr const & a1, expr const & a2, expr const & a3, tag g = nulltag) const;
-    expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
-                    tag g = nulltag) const;
-    expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
-                    expr const & a5, tag g = nulltag) const;
-    expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
-                    expr const & a5, expr const & a6, tag g = nulltag) const;
-    expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
-                    expr const & a5, expr const & a6, expr const & a7, tag g = nulltag) const;
-    expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
-                    expr const & a5, expr const & a6, expr const & a7, expr const & a8,
-                    tag g = nulltag) const;
 };
 
 expr copy_tag(expr const & e, expr && new_e);
@@ -460,14 +445,14 @@ expr mk_app(unsigned num_args, expr const * args, tag g = nulltag);
 inline expr mk_app(std::initializer_list<expr> const & l, tag g = nulltag) {
     return mk_app(l.size(), l.begin(), g);
 }
-template<typename T> expr mk_app(T const & args, tag g = nulltag) { return mk_app(args.size(), args.data(), g); }
-template<typename T> expr mk_app(expr const & f, T const & args, tag g = nulltag) {
+inline expr mk_app(buffer<expr> const & args, tag g = nulltag) { return mk_app(args.size(), args.data(), g); }
+inline expr mk_app(expr const & f, buffer<expr> const & args, tag g = nulltag) {
     return mk_app(f, args.size(), args.data(), g);
 }
 expr mk_rev_app(expr const & f, unsigned num_args, expr const * args, tag g = nulltag);
 expr mk_rev_app(unsigned num_args, expr const * args, tag g = nulltag);
-template<typename T> expr mk_rev_app(T const & args, tag g = nulltag) { return mk_rev_app(args.size(), args.data(), g); }
-template<typename T> expr mk_rev_app(expr const & f, T const & args, tag g = nulltag) {
+inline expr mk_rev_app(buffer<expr> const & args, tag g = nulltag) { return mk_rev_app(args.size(), args.data(), g); }
+inline expr mk_rev_app(expr const & f, buffer<expr> const & args, tag g = nulltag) {
     return mk_rev_app(f, args.size(), args.data(), g);
 }
 expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e,
@@ -505,34 +490,6 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const
                    tag g = nulltag) {
     return mk_app({e1, e2, e3, e4, e5}, g);
 }
-inline expr expr::operator()(expr const & a, tag g) const {
-    return mk_app({*this, a}, g);
-}
-inline expr expr::operator()(expr const & a1, expr const & a2, tag g) const {
-    return mk_app({*this, a1, a2}, g);
-}
-inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, tag g) const {
-    return mk_app({*this, a1, a2, a3}, g);
-}
-inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, tag g) const {
-    return mk_app({*this, a1, a2, a3, a4}, g);
-}
-inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
-                             expr const & a5, tag g) const {
-    return mk_app({*this, a1, a2, a3, a4, a5}, g);
-}
-inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
-                             expr const & a6, tag g) const {
-    return mk_app({*this, a1, a2, a3, a4, a5, a6}, g);
-}
-inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
-                             expr const & a6, expr const & a7, tag g) const {
-    return mk_app({*this, a1, a2, a3, a4, a5, a6, a7}, g);
-}
-inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
-                             expr const & a6, expr const & a7, expr const & a8, tag g) const {
-    return mk_app({*this, a1, a2, a3, a4, a5, a6, a7, a8}, g);
-}
 
 /** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */
 expr mk_app_vars(expr const & f, unsigned n, tag g = nulltag);
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index df4a0ebdf..0a42f4e71 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -74,12 +74,12 @@ static void tst1() {
     expr c  = mk_local("c", Prop);
     expr id = Const("id");
     type_checker checker(env3, name_generator("tmp"));
-    lean_assert(checker.check(id(Prop)).first == Prop >> Prop);
-    lean_assert(checker.whnf(id(Prop, c)).first == c);
-    lean_assert(checker.whnf(id(Prop, id(Prop, id(Prop, c)))).first == c);
+    lean_assert(checker.check(mk_app(id, Prop)).first == Prop >> Prop);
+    lean_assert(checker.whnf(mk_app(id, Prop, c)).first == c);
+    lean_assert(checker.whnf(mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c)))).first == c);
 
     type_checker checker2(env2, name_generator("tmp"));
-    lean_assert(checker2.whnf(id(Prop, id(Prop, id(Prop, c)))).first == id(Prop, id(Prop, id(Prop, c))));
+    lean_assert(checker2.whnf(mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c)))).first == mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c))));
 }
 
 static void tst2() {
@@ -92,7 +92,7 @@ static void tst2() {
     for (unsigned i = 1; i <= 100; i++) {
         expr prev = Const(name(base, i-1));
         env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Prop >> (Prop >> Prop),
-                                          Fun({x, y}, prev(prev(x, y), prev(y, x)))));
+                                          Fun({x, y}, mk_app(prev, mk_app(prev, x, y), mk_app(prev, y, x)))));
     }
     expr Type = mk_Type();
     expr A = Local("A", Type);
@@ -108,10 +108,10 @@ static void tst2() {
     expr c1  =  mk_local("c1", Prop);
     expr c2  = mk_local("c2", Prop);
     expr id = Const("id");
-    std::cout << checker.whnf(f3(c1, c2)).first << "\n";
+    std::cout << checker.whnf(mk_app(f3, c1, c2)).first << "\n";
     lean_assert_eq(env.find(name(base, 98))->get_weight(), 98);
-    lean_assert(checker.is_def_eq(f98(c1, c2), f97(f97(c1, c2), f97(c2, c1))).first);
-    lean_assert(checker.is_def_eq(f98(c1, id(Prop, id(Prop, c2))), f97(f97(c1, id(Prop, c2)), f97(c2, c1))).first);
+    lean_assert(checker.is_def_eq(mk_app(f98, c1, c2), mk_app(f97, mk_app(f97, c1, c2), mk_app(f97, c2, c1))).first);
+    lean_assert(checker.is_def_eq(mk_app(f98, c1, mk_app(id, Prop, mk_app(id, Prop, c2))), mk_app(f97, mk_app(f97, c1, mk_app(id, Prop, c2)), mk_app(f97, c2, c1))).first);
     name_set s;
     s.insert(name(base, 96));
 }
@@ -152,7 +152,7 @@ static void tst3() {
     expr a = Const("a");
     expr b = Const("b");
     type_checker checker(env, name_generator("tmp"));
-    lean_assert_eq(checker.whnf(proj1(proj1(mk(id(A, mk(a, b)), b)))).first, a);
+    lean_assert_eq(checker.whnf(mk_app(proj1, mk_app(proj1, mk_app(mk, mk_app(id, A, mk_app(mk, a, b)), b)))).first, a);
 }
 
 class dummy_ext : public environment_extension {};
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 4e81ef1b9..bbbd95dff 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -44,22 +44,22 @@ static void tst1() {
     a = Const("a");
     expr f;
     f = Var(0);
-    expr fa = f(a);
+    expr fa = mk_app(f, a);
     expr Type = mk_Type();
     expr ty = Type;
     std::cout << fa << "\n";
-    std::cout << fa(a) << "\n";
+    std::cout << mk_app(fa, a) << "\n";
     lean_assert(is_eqp(app_fn(fa), f));
     lean_assert(is_eqp(app_arg(fa), a));
     {
         scoped_expr_caching set(false);
-        lean_assert(!is_eqp(fa, f(a)));
+        lean_assert(!is_eqp(fa, mk_app(f, a)));
     }
-    lean_assert(fa(a) == f(a, a));
-    std::cout << fa(fa, fa) << "\n";
+    lean_assert(mk_app(fa, a) == mk_app(f, a, a));
+    std::cout << mk_app(fa, fa, fa) << "\n";
     std::cout << mk_lambda("x", ty, Var(0)) << "\n";
-    lean_assert(f(a)(a) == f(a, a));
-    lean_assert(f(a(a)) != f(a, a));
+    lean_assert(mk_app(mk_app(f, a), a) == mk_app(f, a, a));
+    lean_assert(mk_app(f, mk_app(a, a)) != mk_app(f, a, a));
     lean_assert(mk_lambda("x", ty, Var(0)) == mk_lambda("y", ty, Var(0)));
     std::cout << mk_pi("x", ty, Var(0)) << "\n";
 }
@@ -69,7 +69,7 @@ static expr mk_dag(unsigned depth, bool _closed = false) {
     expr a = _closed ? Const("a") : Var(0);
     while (depth > 0) {
         depth--;
-        a = f(a, a);
+        a = mk_app(f, a, a);
     }
     return a;
 }
@@ -86,7 +86,7 @@ static expr mk_big(expr f, unsigned depth, unsigned val) {
     if (depth == 1)
         return Const(name(name("foo"), val));
     else
-        return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
+        return mk_app(f, mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
 }
 
 static void tst3() {
@@ -101,7 +101,7 @@ static void tst4() {
     expr f = Const("f");
     expr a = Var(0);
     for (unsigned i = 0; i < 10000; i++) {
-        a = f(a);
+        a = mk_app(f, a);
     }
 }
 
@@ -109,7 +109,7 @@ static expr mk_redundant_dag(expr f, unsigned depth) {
     if (depth == 0)
         return Var(0);
     else
-        return f(mk_redundant_dag(f, depth - 1), mk_redundant_dag(f, depth - 1));
+        return mk_app(f, mk_redundant_dag(f, depth - 1), mk_redundant_dag(f, depth - 1));
 }
 
 static unsigned count_core(expr const & a, expr_set & s) {
@@ -170,10 +170,10 @@ static void tst7() {
     scoped_expr_caching set(false);
     expr f  = Const("f");
     expr v  = Var(0);
-    expr a1 = max_sharing(f(v, v));
-    expr a2 = max_sharing(f(v, v));
+    expr a1 = max_sharing(mk_app(f, v, v));
+    expr a2 = max_sharing(mk_app(f, v, v));
     lean_assert(!is_eqp(a1, a2));
-    expr b  = max_sharing(f(a1, a2));
+    expr b  = max_sharing(mk_app(f, a1, a2));
     lean_assert(is_eqp(app_arg(app_fn(b)), app_arg(b)));
 }
 
@@ -188,16 +188,16 @@ static void tst8() {
     lean_assert(closed(a));
     lean_assert(!closed(x));
     lean_assert(closed(f));
-    lean_assert(!closed(f(x)));
+    lean_assert(!closed(mk_app(f, x)));
     lean_assert(closed(mk_lambda("x", p, x)));
     lean_assert(!closed(mk_lambda("x", x, x)));
     lean_assert(!closed(mk_lambda("x", p, y)));
-    lean_assert(closed(f(f(f(a)))));
-    lean_assert(closed(mk_lambda("x", p, f(f(f(a))))));
+    lean_assert(closed(mk_app(f, mk_app(f, mk_app(f, a)))));
+    lean_assert(closed(mk_lambda("x", p, mk_app(f, mk_app(f, mk_app(f, a))))));
     lean_assert(closed(mk_pi("x", p, x)));
     lean_assert(!closed(mk_pi("x", x, x)));
     lean_assert(!closed(mk_pi("x", p, y)));
-    lean_assert(closed(mk_pi("x", p, f(f(f(a))))));
+    lean_assert(closed(mk_pi("x", p, mk_app(f, mk_app(f, mk_app(f, a))))));
     lean_assert(closed(mk_lambda("y", p, mk_lambda("x", p, y))));
     lean_assert(closed(mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}))));
     expr r = mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}));
@@ -243,25 +243,25 @@ static void tst11() {
     expr y = Var(1);
     expr Type = mk_Type();
     expr t = Type;
-    std::cout << instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) << "\n";
-    lean_assert(instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) ==
-                mk_lambda("x", t, f(f(f(a), b), f(x, f(a)))));
-    std::cout << abstract(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) << "\n";
-    lean_assert(abstract(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) ==
-                mk_lambda("x", t, f(Var(1), mk_lambda("y", t, f(b, Var(2))))));
-    lean_assert(substitute(f(f(f(a))), f(a), b) == f(f(b)));
+    std::cout << instantiate(mk_lambda("x", t, mk_app(f, mk_app(f, y, b), mk_app(f, x, y))), mk_app(f, a)) << "\n";
+    lean_assert(instantiate(mk_lambda("x", t, mk_app(f, mk_app(f, y, b), mk_app(f, x, y))), mk_app(f, a)) ==
+                mk_lambda("x", t, mk_app(f, mk_app(f, mk_app(f, a), b), mk_app(f, x, mk_app(f, a)))));
+    std::cout << abstract(mk_lambda("x", t, mk_app(f, a, mk_lambda("y", t, mk_app(f, b, a)))), Const("a")) << "\n";
+    lean_assert(abstract(mk_lambda("x", t, mk_app(f, a, mk_lambda("y", t, mk_app(f, b, a)))), Const("a")) ==
+                mk_lambda("x", t, mk_app(f, Var(1), mk_lambda("y", t, mk_app(f, b, Var(2))))));
+    lean_assert(substitute(mk_app(f, mk_app(f, mk_app(f, a))), mk_app(f, a), b) == mk_app(f, mk_app(f, b)));
 }
 
 static void tst12() {
     scoped_expr_caching set(false);
     expr f  = Const("f");
     expr v  = Var(0);
-    expr a1 = max_sharing(f(v, v));
-    expr a2 = max_sharing(f(v, v));
+    expr a1 = max_sharing(mk_app(f, v, v));
+    expr a2 = max_sharing(mk_app(f, v, v));
     lean_assert(!is_eqp(a1, a2));
     lean_assert(a1 == a2);
     max_sharing_fn M;
-    lean_assert(is_eqp(M(f(v, v)), M(f(v, v))));
+    lean_assert(is_eqp(M(mk_app(f, v, v)), M(mk_app(f, v, v))));
     lean_assert(is_eqp(M(a1), M(a2)));
 }
 
@@ -292,9 +292,9 @@ static void tst15() {
     expr m = mk_metavar("m", Prop);
     check_serializer(m);
     lean_assert(has_metavar(m));
-    lean_assert(has_metavar(f(m)));
-    lean_assert(!has_metavar(f(a)));
-    lean_assert(!has_metavar(f(x)));
+    lean_assert(has_metavar(mk_app(f, m)));
+    lean_assert(!has_metavar(mk_app(f, a)));
+    lean_assert(!has_metavar(mk_app(f, x)));
     lean_assert(!has_metavar(Pi(a, a)));
     lean_assert(!has_metavar(Type));
     lean_assert(!has_metavar(Fun(a, a)));
@@ -303,9 +303,9 @@ static void tst15() {
     lean_assert(has_metavar(Pi(a1, a1)));
     lean_assert(has_metavar(Fun(a, m)));
     lean_assert(has_metavar(Fun(a1, a)));
-    lean_assert(has_metavar(f(a, a, m)));
-    lean_assert(has_metavar(f(a, m, a, a)));
-    lean_assert(!has_metavar(f(a, a, a, a)));
+    lean_assert(has_metavar(mk_app(f, a, a, m)));
+    lean_assert(has_metavar(mk_app(f, a, m, a, a)));
+    lean_assert(!has_metavar(mk_app(f, a, a, a, a)));
 }
 
 static void check_copy(expr const & e) {
@@ -319,7 +319,7 @@ static void check_copy(expr const & e) {
 static void tst16() {
     expr f = Const("f");
     expr a = Const("a");
-    check_copy(f(a));
+    check_copy(mk_app(f, a));
     expr Prop = mk_Prop();
     check_copy(mk_metavar("M", Prop));
     check_copy(mk_lambda("x", a, Var(0)));
@@ -356,10 +356,10 @@ static void tst18() {
     check_serializer(l);
     lean_assert(!has_local(m));
     lean_assert(has_local(l));
-    lean_assert(!has_local(f(m)));
-    lean_assert(has_local(f(l)));
-    lean_assert(!has_local(f(a0)));
-    lean_assert(!has_local(f(x)));
+    lean_assert(!has_local(mk_app(f, m)));
+    lean_assert(has_local(mk_app(f, l)));
+    lean_assert(!has_local(mk_app(f, a0)));
+    lean_assert(!has_local(mk_app(f, x)));
     lean_assert(!has_local(Pi(a, a)));
     lean_assert(!has_local(Pi(a1, a1)));
     lean_assert(!has_local(Type));
@@ -369,9 +369,9 @@ static void tst18() {
     lean_assert(has_local(Pi(a2, a2)));
     lean_assert(has_local(Fun(a, l)));
     lean_assert(has_local(Fun(a2, a2)));
-    lean_assert(has_local(f(a, a, l)));
-    lean_assert(has_local(f(a, l, a, a)));
-    lean_assert(!has_local(f(a0, a0, a0, a0)));
+    lean_assert(has_local(mk_app(f, a, a, l)));
+    lean_assert(has_local(mk_app(f, a, l, a, a)));
+    lean_assert(!has_local(mk_app(f, a0, a0, a0, a0)));
 }
 
 int main() {
diff --git a/src/tests/kernel/free_vars.cpp b/src/tests/kernel/free_vars.cpp
index a138e559a..7318ba573 100644
--- a/src/tests/kernel/free_vars.cpp
+++ b/src/tests/kernel/free_vars.cpp
@@ -19,16 +19,16 @@ static void tst1() {
     expr x = Var(0);
     expr y = Var(1);
     expr t = Const("t");
-    expr F = mk_lambda("_", t, f(x));
-    lean_assert(has_free_var(mk_lambda("_", t, f(Var(1))), 0));
-    lean_assert(!has_free_var(mk_lambda("_", t, f(Var(0))), 1));
-    lean_assert(!has_free_var(mk_pi("_", t, mk_lambda("_", t, f(Var(1)))), 0));
-    lean_assert(has_free_var(f(Var(0)), 0));
-    lean_assert(has_free_var(f(Var(1)), 1));
-    lean_assert(!has_free_var(f(Var(1)), 0));
-    lean_assert_eq(lower_free_vars(f(Var(1)), 1), f(Var(0)));
-    lean_assert_eq(lower_free_vars(mk_lambda("_", t, f(Var(2))), 1), mk_lambda("_", t, f(Var(1))));
-    lean_assert_eq(lower_free_vars(mk_lambda("_", t, f(Var(0))), 1), mk_lambda("_", t, f(Var(0))));
+    expr F = mk_lambda("_", t, mk_app(f, x));
+    lean_assert(has_free_var(mk_lambda("_", t, mk_app(f, Var(1))), 0));
+    lean_assert(!has_free_var(mk_lambda("_", t, mk_app(f, Var(0))), 1));
+    lean_assert(!has_free_var(mk_pi("_", t, mk_lambda("_", t, mk_app(f, Var(1)))), 0));
+    lean_assert(has_free_var(mk_app(f, Var(0)), 0));
+    lean_assert(has_free_var(mk_app(f, Var(1)), 1));
+    lean_assert(!has_free_var(mk_app(f, Var(1)), 0));
+    lean_assert_eq(lower_free_vars(mk_app(f, Var(1)), 1), mk_app(f, Var(0)));
+    lean_assert_eq(lower_free_vars(mk_lambda("_", t, mk_app(f, Var(2))), 1), mk_lambda("_", t, mk_app(f, Var(1))));
+    lean_assert_eq(lower_free_vars(mk_lambda("_", t, mk_app(f, Var(0))), 1), mk_lambda("_", t, mk_app(f, Var(0))));
 }
 
 static void tst2() {
@@ -46,7 +46,7 @@ static void tst3() {
     unsigned m = 10;
     expr f = Const("f");
     expr a = Const("a");
-    expr r = f(a, Var(m));
+    expr r = mk_app(f, a, Var(m));
     expr b = Const("Prop");
     for (unsigned i = 0; i < n; i++)
         r = mk_lambda(name(), b, r);
@@ -63,11 +63,11 @@ static void tst4() {
     expr B = mk_Prop();
     expr x = Local("x", B);
     expr y = Local("y", B);
-    expr t = f(Fun({x, y}, f(x, y))(f(Var(1), Var(2))), x);
+    expr t = mk_app(f, mk_app(Fun({x, y}, mk_app(f, x, y)), mk_app(f, Var(1), Var(2))), x);
     lean_assert_eq(lift_free_vars(t, 1, 2),
-                   f(Fun(x, Fun(y, f(x, y)))(f(Var(3), Var(4))), x));
+                   mk_app(f, mk_app(Fun(x, Fun(y, mk_app(f, x, y))), mk_app(f, Var(3), Var(4))), x));
     lean_assert_eq(lift_free_vars(t, 0, 3),
-                   f(Fun(x, Fun(y, f(x, y)))(f(Var(4), Var(5))), x));
+                   mk_app(f, mk_app(Fun(x, Fun(y, mk_app(f, x, y))), mk_app(f, Var(4), Var(5))), x));
     lean_assert_eq(lift_free_vars(t, 3, 2), t);
 }
 
diff --git a/src/tests/kernel/instantiate.cpp b/src/tests/kernel/instantiate.cpp
index 7ed456265..aebbf5400 100644
--- a/src/tests/kernel/instantiate.cpp
+++ b/src/tests/kernel/instantiate.cpp
@@ -23,16 +23,16 @@ static void tst1() {
     expr b = Const("b");
     expr c = Const("c");
     expr d = Const("d");
-    expr F1 = Fun(x, x)(f, a);
+    expr F1 = mk_app(Fun(x, x), f, a);
     lean_assert(is_head_beta(F1));
-    lean_assert_eq(head_beta_reduce(F1), f(a));
-    expr F2 = Fun({h, y}, h(y))(f, a, b, c);
+    lean_assert_eq(head_beta_reduce(F1), mk_app(f, a));
+    expr F2 = mk_app(Fun({h, y}, mk_app(h, y)), f, a, b, c);
     lean_assert(is_head_beta(F2));
-    lean_assert_eq(head_beta_reduce(F2), f(a, b, c));
-    expr F3 = Fun(x, f(Fun(y, y)(x), x))(a);
+    lean_assert_eq(head_beta_reduce(F2), mk_app(f, a, b, c));
+    expr F3 = mk_app(Fun(x, mk_app(f, mk_app(Fun(y, y), x), x)), a);
     lean_assert(is_head_beta(F3));
-    lean_assert(head_beta_reduce(F3) == f(Fun(y, y)(a), a));
-    lean_assert(beta_reduce(F3) == f(a, a));
+    lean_assert(head_beta_reduce(F3) == mk_app(f, mk_app(Fun(y, y), a), a));
+    lean_assert(beta_reduce(F3) == mk_app(f, a, a));
 }
 
 int main() {
diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp
index e6cbb5fb7..e1773a1f7 100644
--- a/src/tests/kernel/max_sharing.cpp
+++ b/src/tests/kernel/max_sharing.cpp
@@ -24,7 +24,7 @@ static void tst1() {
     expr y = Local("y", N);
     expr f = Const("f");
     expr F1, F2;
-    F1 = f(Fun(x, f(x, x)), Fun(y, f(y, y)));
+    F1 = mk_app(f, Fun(x, mk_app(f, x, x)), Fun(y, mk_app(f, y, y)));
     lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1)));
     F2 = max_fn(F1);
     std::cout << F2 << "\n";
@@ -38,8 +38,8 @@ static void tst2() {
     expr x   = Const("x");
     expr f   = Const("f");
     expr g   = Const("g");
-    expr t1  = max_fn2(max_fn1(f(g(x))));
-    expr t2  = max_fn2(f(t1, g(x)));
+    expr t1  = max_fn2(max_fn1(mk_app(f, mk_app(g, x))));
+    expr t2  = max_fn2(mk_app(f, t1, mk_app(g, x)));
     expr arg1 = app_arg(app_arg(app_fn(t2)));
     expr arg2 = app_arg(t2);
     lean_assert(is_eqp(arg1, arg2));
@@ -54,11 +54,11 @@ static void tst3() {
     expr f  = Const("f");
     expr new_a1 = max_fn(a1);
     lean_assert(is_eqp(new_a1, a1));
-    expr t1 = max_fn(f(a2));
+    expr t1 = max_fn(mk_app(f, a2));
     lean_assert(is_eqp(app_arg(t1), a1));
-    expr t2 = max_fn(f(a2));
+    expr t2 = max_fn(mk_app(f, a2));
     lean_assert(is_eqp(t1, t2));
-    expr t3 = max_fn(f(a3));
+    expr t3 = max_fn(mk_app(f, a3));
     lean_assert(is_eqp(t1, t3));
 }
 
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index 2f20c287b..a80177bfd 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -81,11 +81,11 @@ static void tst1() {
     lean_assert(m1 != m2);
     expr f = Const("f");
     expr a = Const("a");
-    subst.assign(m1, f(a));
+    subst.assign(m1, mk_app(f, a));
     lean_assert(subst.is_assigned(m1));
     lean_assert(!subst.is_assigned(m2));
-    lean_assert(*subst.get_expr(m1) == f(a));
-    lean_assert(subst.instantiate_metavars(f(m1)).first == f(f(a)));
+    lean_assert(*subst.get_expr(m1) == mk_app(f, a));
+    lean_assert(subst.instantiate_metavars(mk_app(f, m1)).first == mk_app(f, mk_app(f, a)));
     std::cout << subst << "\n";
 }
 
@@ -98,19 +98,19 @@ static void tst2() {
     expr f = Const("f");
     expr g = Const("g");
     expr a = Const("a");
-    s.assign(m1, f(m2), mk_assumption_justification(1));
-    s.assign(m2, g(a),  mk_assumption_justification(2));
+    s.assign(m1, mk_app(f, m2), mk_assumption_justification(1));
+    s.assign(m2, mk_app(g, a),  mk_assumption_justification(2));
     lean_assert(check_assumptions(s.get_assignment(m1)->second, {1}));
-    lean_assert(s.occurs(m1, f(m1)));
-    lean_assert(s.occurs(m2, f(m1)));
-    lean_assert(!s.occurs(m1, f(m2)));
-    lean_assert(!s.occurs(m1, f(a)));
-    lean_assert(!s.occurs(m3, f(m1)));
+    lean_assert(s.occurs(m1, mk_app(f, m1)));
+    lean_assert(s.occurs(m2, mk_app(f, m1)));
+    lean_assert(!s.occurs(m1, mk_app(f, m2)));
+    lean_assert(!s.occurs(m1, mk_app(f, a)));
+    lean_assert(!s.occurs(m3, mk_app(f, m1)));
     std::cout << s << "\n";
-    auto p1 = s.instantiate_metavars(g(m1));
+    auto p1 = s.instantiate_metavars(mk_app(g, m1));
     check_assumptions(p1.second, {1, 2});
     lean_assert(check_assumptions(s.get_assignment(m1)->second, {1, 2}));
-    lean_assert(p1.first == g(f(g(a))));
+    lean_assert(p1.first == mk_app(g, mk_app(f, mk_app(g, a))));
 }
 
 static void tst3() {
@@ -123,11 +123,11 @@ static void tst3() {
     expr b  = Const("b");
     expr x  = Local("x", Prop);
     expr y  = Local("y", Prop);
-    s.assign(m1, Fun({x, y}, f(y, x)));
-    lean_assert_eq(s.instantiate_metavars(m1(a, b, g(a))).first, f(b, a, g(a)));
-    lean_assert_eq(s.instantiate_metavars(m1(a)).first, Fun(y, f(y, a)));
-    lean_assert_eq(s.instantiate_metavars(m1(a, b)).first, f(b, a));
-    std::cout << s.instantiate_metavars(m1(a, b, g(a))).first << "\n";
+    s.assign(m1, Fun({x, y}, mk_app(f, y, x)));
+    lean_assert_eq(s.instantiate_metavars(mk_app(m1, a, b, mk_app(g, a))).first, mk_app(f, b, a, mk_app(g, a)));
+    lean_assert_eq(s.instantiate_metavars(mk_app(m1, a)).first, Fun(y, mk_app(f, y, a)));
+    lean_assert_eq(s.instantiate_metavars(mk_app(m1, a, b)).first, mk_app(f, b, a));
+    std::cout << s.instantiate_metavars(mk_app(m1, a, b, mk_app(g, a))).first << "\n";
 }
 
 static void tst4() {
@@ -143,13 +143,13 @@ static void tst4() {
     expr a  = Const("a");
     expr T1 = mk_sort(l1);
     expr T2 = mk_sort(u);
-    expr t  = f(T1, T2, m1, m2);
+    expr t  = mk_app(f, T1, T2, m1, m2);
     lean_assert(s.instantiate_metavars(t).first == t);
     s.assign(m1, a, justification());
     s.assign(m2, m3, justification());
-    lean_assert(s.instantiate_metavars(t).first == f(T1, T2, a, m3));
+    lean_assert(s.instantiate_metavars(t).first == mk_app(f, T1, T2, a, m3));
     s.assign(l1, level(), justification());
-    lean_assert(s.instantiate_metavars(t).first == f(Prop, T2, a, m3));
+    lean_assert(s.instantiate_metavars(t).first == mk_app(f, Prop, T2, a, m3));
 }
 
 int main() {
diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp
index 3aba1521d..eb9c8d86e 100644
--- a/src/tests/kernel/replace.cpp
+++ b/src/tests/kernel/replace.cpp
@@ -22,7 +22,7 @@ expr mk_big(expr f, unsigned depth, unsigned val) {
     if (depth == 1)
         return mk_constant(name(name("foo"), val));
     else
-        return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
+        return mk_app(f, mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
 }
 
 static void tst1() {
diff --git a/src/tests/library/deep_copy.cpp b/src/tests/library/deep_copy.cpp
index d8c0217a8..dfa2c6d9e 100644
--- a/src/tests/library/deep_copy.cpp
+++ b/src/tests/library/deep_copy.cpp
@@ -22,7 +22,7 @@ static void tst1() {
     expr t = Type;
     expr z = Const("z");
     expr m = mk_metavar("a", Type);
-    expr F = mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), f(x, m))));
+    expr F = mk_pi("y", t, mk_lambda("x", t, mk_app(f, mk_app(f, mk_app(f, x, a), Const("10")), mk_app(f, x, m))));
     expr G = deep_copy(F);
     lean_assert(F == G);
     lean_assert(!is_eqp(F, G));
diff --git a/src/tests/library/expr_lt.cpp b/src/tests/library/expr_lt.cpp
index ed16125dc..5412b47be 100644
--- a/src/tests/library/expr_lt.cpp
+++ b/src/tests/library/expr_lt.cpp
@@ -20,15 +20,15 @@ static void tst1() {
     lt(Const("a"), Const("b"), true);
     lt(Const("a"), Const("a"), false);
     lt(Var(1), Const("a"), true);
-    lt(Const("f")(Var(0)), Const("f")(Var(0), Const("a")), true);
-    lt(Const("f")(Var(0), Const("a"), Const("b")), Const("f")(Var(0), Const("a")), false);
-    lt(Const("f")(Var(0), Const("a")), Const("g")(Var(0), Const("a")), true);
-    lt(Const("f")(Var(0), Const("a")), Const("f")(Var(1), Const("a")), true);
-    lt(Const("f")(Var(0), Const("a")), Const("f")(Var(0), Const("b")), true);
-    lt(Const("f")(Var(0), Const("a")), Const("f")(Var(0), Const("a")), false);
-    lt(Const("g")(Var(0), Const("a")), Const("f")(Var(0), Const("a")), false);
-    lt(Const("f")(Var(1), Const("a")), Const("f")(Var(0), Const("a")), false);
-    lt(Const("f")(Var(0), Const("b")), Const("f")(Var(0), Const("a")), false);
+    lt(mk_app(Const("f"), Var(0)), mk_app(Const("f"), Var(0), Const("a")), true);
+    lt(mk_app(Const("f"), Var(0), Const("a"), Const("b")), mk_app(Const("f"), Var(0), Const("a")), false);
+    lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("g"), Var(0), Const("a")), true);
+    lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("f"), Var(1), Const("a")), true);
+    lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("f"), Var(0), Const("b")), true);
+    lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("f"), Var(0), Const("a")), false);
+    lt(mk_app(Const("g"), Var(0), Const("a")), mk_app(Const("f"), Var(0), Const("a")), false);
+    lt(mk_app(Const("f"), Var(1), Const("a")), mk_app(Const("f"), Var(0), Const("a")), false);
+    lt(mk_app(Const("f"), Var(0), Const("b")), mk_app(Const("f"), Var(0), Const("a")), false);
 }
 
 int main() {
diff --git a/src/tests/library/head_map.cpp b/src/tests/library/head_map.cpp
index dd6be7d34..cf71bdb28 100644
--- a/src/tests/library/head_map.cpp
+++ b/src/tests/library/head_map.cpp
@@ -21,7 +21,7 @@ static void tst1() {
     expr Prop = mk_Prop();
     expr x = Local("x", Prop);
     expr l1 = Fun(x, x);
-    expr l2 = Fun(x, f(x));
+    expr l2 = Fun(x, mk_app(f, x));
     lean_assert(l1 != l2);
     lean_assert(map.empty());
     map.insert(a, a);
@@ -52,9 +52,9 @@ static void tst1() {
     map.erase(a);
     lean_assert(size_fn(map) == 0);
     lean_assert(map.empty());
-    map.insert(f(a), f(a));
-    map.insert(f(b), f(b));
-    lean_assert(length(*map.find(f(a))) == 2);
+    map.insert(mk_app(f, a), mk_app(f, a));
+    map.insert(mk_app(f, b), mk_app(f, b));
+    lean_assert(length(*map.find(mk_app(f, a))) == 2);
 }
 
 int main() {
diff --git a/src/tests/library/occurs.cpp b/src/tests/library/occurs.cpp
index 66a21b026..4b94481f3 100644
--- a/src/tests/library/occurs.cpp
+++ b/src/tests/library/occurs.cpp
@@ -22,10 +22,10 @@ static void tst1() {
     expr a1 = Local("a", T);
     lean_assert(occurs(f, f));
     lean_assert(!occurs(a, f));
-    lean_assert(occurs(a, f(a)));
-    lean_assert(occurs("a", f(a)));
+    lean_assert(occurs(a, mk_app(f, a)));
+    lean_assert(occurs("a", mk_app(f, a)));
     lean_assert(!occurs("b", f));
-    lean_assert(!occurs(a, Fun(a1, f(a1))));
+    lean_assert(!occurs(a, Fun(a1, mk_app(f, a1))));
 }
 
 int main() {
diff --git a/src/tests/library/unifier.cpp b/src/tests/library/unifier.cpp
index 1c6bf0a18..e97192d0c 100644
--- a/src/tests/library/unifier.cpp
+++ b/src/tests/library/unifier.cpp
@@ -21,8 +21,8 @@ static void tst1() {
     expr a  = Local("a", A);
     expr b  = Local("b", A);
     expr m  = mk_metavar("m", A);
-    expr t1 = f(m, m);
-    expr t2 = f(a, b);
+    expr t1 = mk_app(f, m, m);
+    expr t2 = mk_app(f, a, b);
     auto r = unify(env, t1, t2, ngen, false);
     lean_assert(!r.pull());
 }