diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index b11ce3f12..36242a518 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -129,11 +129,8 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
             first = false;
         else
             p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
-        if (p.curr_is_token(get_end_tk())) {
-            auto pos = p.pos();
-            p.next();
-            throw parser_error("invalid 'begin-end' expression, tactic or expression expected", pos);
-        }
+        if (p.curr_is_token(get_end_tk()))
+            break;
         bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
                           p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
                           p.curr_is_token(get_fun_tk()));
diff --git a/tests/lean/run/beginend2.lean b/tests/lean/run/beginend2.lean
new file mode 100644
index 000000000..9febd3358
--- /dev/null
+++ b/tests/lean/run/beginend2.lean
@@ -0,0 +1,13 @@
+import hott.path tools.tactic
+
+open path tactic
+open path (induction_on)
+
+definition concat_whisker2 {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
+  (whiskerR a q) @ (whiskerL p' b) ≈ (whiskerL p b) @ (whiskerR a q') :=
+begin
+  apply (induction_on b),
+  apply (induction_on a),
+  apply ((concat_1p _)^),
+end
+exit