diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 4559586f3..a0805110b 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -296,9 +296,10 @@ public: } void execute(cmd_context & ctx) override { - if (!m_tactic) { + if (!m_tactic) throw cmd_exception("apply needs a tactic argument"); - } + if (ctx.ignore_check()) + return; params_ref p = ctx.params().merge_default_params(ps()); tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p); {