diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp
index 766195b90a..6080071af8 100644
--- a/src/frontends/lean/parse_rewrite_tactic.cpp
+++ b/src/frontends/lean/parse_rewrite_tactic.cpp
@@ -135,14 +135,14 @@ static expr parse_rewrite_element(parser & p, bool use_paren) {
 void parse_rewrite_tactic_elems(parser & p, buffer<expr> & elems) {
     if (p.curr_is_token(get_lbracket_tk())) {
         p.next();
-        while (true) {
+        while (!p.curr_is_token(get_rbracket_tk())) {
             auto pos = p.pos();
             elems.push_back(p.save_pos(parse_rewrite_element(p, false), pos));
             if (!p.curr_is_token(get_comma_tk()))
                 break;
             p.next();
         }
-        p.check_token_next(get_rbracket_tk(), "invalid rewrite tactic, ',' or ']' expected");
+        p.next();
     } else {
         auto pos = p.pos();
         elems.push_back(p.save_pos(parse_rewrite_element(p, true), pos));
diff --git a/tests/lean/run/695d.lean b/tests/lean/run/695d.lean
new file mode 100644
index 0000000000..19fed078b9
--- /dev/null
+++ b/tests/lean/run/695d.lean
@@ -0,0 +1,7 @@
+import data.nat
+open nat
+
+example (a b : nat) : 0 + a + 0 = a :=
+begin
+  rewrite [add_zero, zero_add,]
+end