diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 93a8c1e59..794cc09e6 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -351,14 +351,14 @@ public: } throw tactic_exception(sstream() << "invalid 'induction' tactic, hypothesis '" << m_h_name << "' must have a type that is associated with a recursor"); - } catch (exception & ex) { - if (m_throw_ex) - throw tactic_exception(sstream() << "invalid 'induction' tactic, " << ex.what()); - return optional(); } catch (tactic_exception & ex) { if (m_throw_ex) throw; return optional(); + } catch (exception & ex) { + if (m_throw_ex) + throw tactic_exception(sstream() << "invalid 'induction' tactic, " << ex.what()); + return optional(); } } };