diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 14b62c700..3e26589a7 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -1013,6 +1013,18 @@ optional<unsigned> get_num_minor_premises(environment const & env, name const &
     }
 }
 
+optional<unsigned> get_num_intro_rules(environment const & env, name const & n) {
+    if (auto decls = is_inductive_decl(env, n)) {
+        for (auto const & decl : std::get<2>(*decls)) {
+            if (inductive_decl_name(decl) == n)
+                return some(length(inductive_decl_intros(decl)));
+        }
+        lean_unreachable();
+    } else {
+        return optional<unsigned>();
+    }
+}
+
 bool has_dep_elim(environment const & env, name const & n) {
     inductive_env_ext const & ext = get_extension(env);
     if (auto it = ext.m_elim_info.find(get_elim_name(n)))
diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h
index abf2c5d6b..08a49d9ca 100644
--- a/src/kernel/inductive/inductive.h
+++ b/src/kernel/inductive/inductive.h
@@ -86,6 +86,10 @@ optional<unsigned> get_num_indices(environment const & env, name const & n);
     If \c n is not an inductive datatype in \c env, then return none.
 */
 optional<unsigned> get_num_minor_premises(environment const & env, name const & n);
+/** \brief Return the number of introduction rules in the given inductive datatype.
+    If \c n is not an inductive datatype in \c env, then return none.
+*/
+optional<unsigned> get_num_intro_rules(environment const & env, name const & n);
 /** \brief Return the number of type formers in the given inductive datatype.
     If \c n is not an inductive datatype in \c env, then return none.
 */
diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index 42f5cda62..f111132fa 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -34,7 +34,10 @@ class inversion_tac {
         m_dep_elim      = inductive::has_dep_elim(m_env, n);
         m_nindices      = *inductive::get_num_indices(m_env, n);
         m_nparams       = *inductive::get_num_params(m_env, n);
-        m_nminors       = *inductive::get_num_minor_premises(m_env, n);
+        // This tactic is bases on cases_on construction which only has
+        // minor premises for the introduction rules of this datatype.
+        // For non-mutually recursive datatypes inductive::get_num_intro_rules == inductive::get_num_minor_premises
+        m_nminors       = *inductive::get_num_intro_rules(m_env, n);
         m_I_decl        = m_env.get(n);
         m_cases_on_decl = m_env.get({n, "cases_on"});
     }
diff --git a/tests/lean/run/inv_bug.lean b/tests/lean/run/inv_bug.lean
new file mode 100644
index 000000000..6d5d9fa5f
--- /dev/null
+++ b/tests/lean/run/inv_bug.lean
@@ -0,0 +1,17 @@
+open nat
+open eq.ops
+
+inductive even : nat → Prop :=
+even_zero        : even zero,
+even_succ_of_odd : ∀ {a}, odd a  → even (succ a)
+with odd : nat → Prop :=
+odd_succ_of_even : ∀ {a}, even a → odd (succ a)
+
+example : even 1 → false :=
+begin
+  intro H,
+  cases H with (a, ho),
+  assert (Hz : odd zero),
+  apply (a_eq ▸ ho),
+  inversion Hz
+end