diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index c329d31ab..3690fcb1a 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2025,6 +2025,8 @@ expr parser::parse_tactic_nud() {
         }
     } else if (curr_is_keyword()) {
         return parse_tactic_notation(tactic_nud(), nullptr);
+    } else if (curr_is_numeral() || curr_is_decimal()) {
+        return parse_expr();
     } else {
         throw parser_error("invalid tactic expression", pos());
     }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index cf76e57df..4181303cb 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -357,6 +357,7 @@ public:
     bool curr_is_identifier() const { return curr() == scanner::token_kind::Identifier; }
     /** \brief Return true iff the current token is a numeral */
     bool curr_is_numeral() const { return curr() == scanner::token_kind::Numeral; }
+    bool curr_is_decimal() const { return curr() == scanner::token_kind::Decimal; }
     /** \brief Return true iff the current token is a string */
     bool curr_is_string() const { return curr() == scanner::token_kind::String; }
     /** \brief Return true iff the current token is a keyword */
diff --git a/tests/lean/run/tactic_notation_num_arg_bug.lean b/tests/lean/run/tactic_notation_num_arg_bug.lean
new file mode 100644
index 000000000..7cb1600ef
--- /dev/null
+++ b/tests/lean/run/tactic_notation_num_arg_bug.lean
@@ -0,0 +1,7 @@
+tactic_notation `foo` A := tactic.id
+
+example (a : nat) : a = a :=
+begin
+  foo (10:nat),
+  reflexivity
+end