diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index 1ebce363be..de4f32bf40 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -110,6 +110,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
         name I = r.get_prefix();
         unsigned num_indices  = *inductive::get_num_indices(env, I);
         unsigned num_params   = *inductive::get_num_params(env, I);
+        has_given_major_pos   = true;
         given_major_pos       = num_params + 1 /* motive */ + num_indices;
     }
     declaration d = env.get(r);