diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 42ca4e2976..3a4fed3301 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -245,21 +245,33 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
             value = p.parse_expr();
         } else if (p.curr_is_token(g_colon)) {
             p.next();
+            auto pos = p.pos();
             type = p.parse_expr();
-            p.check_token_next(g_assign, "invalid declaration, ':=' expected");
-            value = p.parse_expr();
+            if (is_theorem && !p.curr_is_token(g_assign)) {
+                value = mk_expr_placeholder();
+            } else {
+                p.check_token_next(g_assign, "invalid declaration, ':=' expected");
+                value = p.save_pos(p.parse_expr(), pos);
+            }
         } else {
             buffer<expr> ps;
             optional<local_environment> lenv;
             lenv = p.parse_binders(ps);
             if (p.curr_is_token(g_colon)) {
                 p.next();
+                auto pos = p.pos();
                 type = p.parse_scoped_expr(ps, *lenv);
+                if (is_theorem && !p.curr_is_token(g_assign)) {
+                    value = p.save_pos(mk_expr_placeholder(), pos);
+                } else {
+                    p.check_token_next(g_assign, "invalid declaration, ':=' expected");
+                    value = p.parse_scoped_expr(ps, *lenv);
+                }
             } else {
                 type = p.save_pos(mk_expr_placeholder(), p.pos());
+                p.check_token_next(g_assign, "invalid declaration, ':=' expected");
+                value = p.parse_scoped_expr(ps, *lenv);
             }
-            p.check_token_next(g_assign, "invalid declaration, ':=' expected");
-            value = p.parse_scoped_expr(ps, *lenv);
             type = p.pi_abstract(ps, type);
             value = p.lambda_abstract(ps, value);
         }
diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean
new file mode 100644
index 0000000000..a2c62baff2
--- /dev/null
+++ b/tests/lean/run/tactic25.lean
@@ -0,0 +1,20 @@
+import standard
+using tactic
+
+definition my_tac1 := apply @refl
+definition my_tac2 := repeat (apply @and_intro; assumption)
+
+tactic_hint my_tac1
+tactic_hint my_tac2
+
+theorem T1 {A : Type.{2}} (a : A) : a = a
+
+theorem T2 {a b c : Bool} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c
+
+definition my_tac3 := fixpoint (λ f, [apply @or_intro_left; f  |
+                                      apply @or_intro_right; f |
+                                      assumption])
+
+tactic_hint [or] my_tac3
+
+theorem T3 {a b c : Bool} (Hb : b) : a ∨ b ∨ c