diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 427835fd8..8e82dca7e 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1391,8 +1391,7 @@ class parser::imp {
             next();
             expr pr      = parse_expr();
             check_rparen_next("invalid apply command, ')' expected");
-            expr pr_type = m_env->infer_type(pr);
-            return ::lean::apply_tactic(pr, pr_type);
+            return ::lean::apply_tactic(pr);
         } else {
            name n = check_identifier_next("invalid apply command, identifier, '(' expr ')', or 'script-block' expected");
            optional<object> o = m_env->find_object(n);
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index db14c618f..410d4c470 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -143,8 +143,9 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
     }
 }
 
-tactic apply_tactic(expr const & th, expr const & th_type, bool all) {
+tactic apply_tactic(expr const & th, bool all) {
     return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
+            expr th_type = type_inferer(env)(th, context(), s.get_menv().copy());
             return apply_tactic(env, s, th, th_type, all);
         });
 }
@@ -161,7 +162,11 @@ tactic apply_tactic(name const & th_name, bool all) {
 
 int mk_apply_tactic(lua_State * L) {
     int nargs = lua_gettop(L);
-    return push_tactic(L, apply_tactic(to_name_ext(L, 1), nargs >= 2 ? lua_toboolean(L, 2) : true));
+    bool all  = nargs >= 2 ? lua_toboolean(L, 2) : true;
+    if (is_expr(L, 1))
+        return push_tactic(L, apply_tactic(to_expr(L, 1), all));
+    else
+        return push_tactic(L, apply_tactic(to_name_ext(L, 1), all));
 }
 
 void open_apply_tactic(lua_State * L) {
diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h
index 3d8f99387..ac09325a4 100644
--- a/src/library/tactic/apply_tactic.h
+++ b/src/library/tactic/apply_tactic.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "library/tactic/tactic.h"
 namespace lean {
-tactic apply_tactic(expr const & th, expr const & th_type, bool all = true);
+tactic apply_tactic(expr const & th, bool all = true);
 tactic apply_tactic(name const & th_name, bool all = true);
 void open_apply_tactic(lua_State * L);
 }