diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index a04dab28e..0f405df64 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -318,19 +318,6 @@ struct lean_extension : public environment_extension {
         env->add_neutral_object(new notation_declaration(new_op, d));
     }
 
-    expr mk_explicit_definition_body(expr type, name const & n, unsigned i, unsigned sz) {
-        if (i == sz) {
-            buffer<expr> args;
-            args.push_back(mk_constant(n));
-            unsigned j = sz;
-            while (j > 0) { --j; args.push_back(mk_var(j)); }
-            return mk_app(args);
-        } else {
-            lean_assert(is_pi(type));
-            return mk_lambda(abst_name(type), abst_domain(type), mk_explicit_definition_body(abst_body(type), n, i+1, sz));
-        }
-    }
-
     static name mk_explicit_name(name const & n) {
         if (n.is_anonymous()) {
             throw exception("anonymous names cannot be used in definitions");
@@ -369,7 +356,7 @@ struct lean_extension : public environment_extension {
             throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', all arguments are explicit");
         std::vector<bool> v(implicit, implicit+sz);
         m_implicit_table[n] = mk_pair(v, explicit_version);
-        expr body = mk_explicit_definition_body(type, n, 0, num_args);
+        expr body = mk_constant(n);
         m_explicit_names.insert(explicit_version);
         env->add_neutral_object(new mark_implicit_command(n, sz, implicit));
         env->auxiliary_section([&]() {
diff --git a/tests/lean/explicit2.lean b/tests/lean/explicit2.lean
new file mode 100644
index 000000000..35b10020d
--- /dev/null
+++ b/tests/lean/explicit2.lean
@@ -0,0 +1,3 @@
+variable f {A : Type} : A → A
+eval (@f Bool)
+eval @f
\ No newline at end of file
diff --git a/tests/lean/explicit2.lean.expected.out b/tests/lean/explicit2.lean.expected.out
new file mode 100644
index 000000000..b6d3e3f24
--- /dev/null
+++ b/tests/lean/explicit2.lean.expected.out
@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+f
+@f