diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index d359388c67..0162c4d5f0 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -321,21 +321,6 @@ struct add_inductive_fn {
         updt_type_checker();
     }
 
-    /** \brief Return true iff \c t is a term of the form (I As t)
-        where I is the inductive datatype being defined, and As are the
-        global parameters of this declaration. */
-    bool is_valid_it_app(expr const & t) {
-        buffer<expr> args;
-        expr I = get_app_args(t, args);
-        if (!is_def_eq(I, m_it_const) || args.size() != m_it_num_args)
-            return false;
-        for (unsigned i = 0; i < m_decl.m_num_params; i++) {
-            if (m_param_consts[i] != args[i])
-                return false;
-        }
-        return true;
-    }
-
     /** \brief Return true iff \c e is the inductive datatype being declared. */
     bool is_it_occ(expr const & e) {
         return is_constant(e) && const_name(e) == const_name(m_it_const);
@@ -346,6 +331,26 @@ struct add_inductive_fn {
         return (bool)find(t, [&](expr const & e, unsigned) { return is_it_occ(e); }); // NOLINT
     }
 
+    /** \brief Return true iff \c t is a term of the form (I As t)
+        where I is the inductive datatype being defined, and As are the
+        global parameters of this declaration. Moreover I does not occur in t */
+    bool is_valid_it_app(expr const & t) {
+        buffer<expr> args;
+        expr I = get_app_args(t, args);
+        if (!is_def_eq(I, m_it_const) || args.size() != m_it_num_args)
+            return false;
+        unsigned i = 0;
+        for (; i < m_decl.m_num_params; i++) {
+            if (m_param_consts[i] != args[i])
+                return false;
+        }
+        for (; i < args.size(); i++) {
+            if (has_it_occ(args[i]))
+                return false;
+        }
+        return true;
+    }
+
     /** \brief Return some(d_idx) iff \c t is a recursive argument, \c d_idx is the index of the recursive inductive datatype.
         Return none otherwise. */
     bool is_rec_argument(expr t) {
diff --git a/tests/lean/bad_index.lean b/tests/lean/bad_index.lean
new file mode 100644
index 0000000000..9074e4ecd7
--- /dev/null
+++ b/tests/lean/bad_index.lean
@@ -0,0 +1,5 @@
+inductive foo1 : Type -> Type
+| mk : foo1 (list (foo1 poly_unit)) -> foo1 (list (foo1 poly_unit))
+
+inductive foo2 : Type -> Type
+| mk : foo2 (foo2 poly_unit) -> foo2 (foo2 poly_unit)
diff --git a/tests/lean/bad_index.lean.expected.out b/tests/lean/bad_index.lean.expected.out
new file mode 100644
index 0000000000..b5455eaa23
--- /dev/null
+++ b/tests/lean/bad_index.lean.expected.out
@@ -0,0 +1,2 @@
+bad_index.lean:1:0: error: arg #1 of 'foo1.mk' contains a non valid occurrence of the datatypes being declared
+bad_index.lean:4:0: error: arg #1 of 'foo2.mk' contains a non valid occurrence of the datatypes being declared
diff --git a/tests/lean/run/mutual_inductive.lean b/tests/lean/run/mutual_inductive.lean
index fa28e6feb4..a4e1dd8e80 100644
--- a/tests/lean/run/mutual_inductive.lean
+++ b/tests/lean/run/mutual_inductive.lean
@@ -174,28 +174,3 @@ check @bar.rec
 check @rig.rec
 
 end X9
-
-namespace X10
-
-mutual_inductive foo, bar, rig
-with foo : Type -> Type
-| mk : bar (foo poly_unit) -> foo (bar poly_unit)
-with bar : Type -> Type
-| mk : foo (bar poly_unit) -> bar (foo poly_unit)
-with rig : Type -> Type
-| mk : foo (bar (rig poly_unit)) -> rig (bar (foo poly_unit)) -> rig (bar (foo poly_unit))
-
-check @foo
-check @bar
-check @rig
-check @foo.rec
-check @bar.rec
-check @rig.rec
-check @foo.has_sizeof_inst
-check @bar.has_sizeof_inst
-check @rig.has_sizeof_inst
-check @foo.mk.sizeof_spec
-check @bar.mk.sizeof_spec
-check @rig.mk.sizeof_spec
-
-end X10