diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp
index 3ac59cb01..a79b5fc60 100644
--- a/src/frontends/lean/parser_expr.cpp
+++ b/src/frontends/lean/parser_expr.cpp
@@ -844,11 +844,10 @@ tactic parser_imp::parse_tactic_expr() {
     if (curr() == scanner::token::ScriptBlock) {
         parse_script_expr();
         return using_script([&](lua_State * L) {
-                try {
+                if (is_tactic(L, -1))
                     return to_tactic(L, -1);
-                } catch (...) {
+                else
                     throw parser_error("invalid script-block, it must return a tactic", p);
-                }
             });
     } else if (curr_is_identifier() && m_tactic_macros && m_tactic_macros->find(curr_name()) != m_tactic_macros->end()) {
         return parse_tactic_macro(curr_name(), p);
diff --git a/tests/lean/tacluacrash.lean b/tests/lean/tacluacrash.lean
new file mode 100644
index 000000000..f630e35fd
--- /dev/null
+++ b/tests/lean/tacluacrash.lean
@@ -0,0 +1,2 @@
+theorem T (a : Bool) : a → a.
+(* foo_tac *)
diff --git a/tests/lean/tacluacrash.lean.expected.out b/tests/lean/tacluacrash.lean.expected.out
new file mode 100644
index 000000000..7e32db3dd
--- /dev/null
+++ b/tests/lean/tacluacrash.lean.expected.out
@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+tacluacrash.lean:2:0: error: invalid script-block, it must return a tactic
+tacluacrash.lean:3:0: error: invalid tactic command, unexpected end of file
+Proof state:
+a : Bool, H : a ⊢ a