src/HOL/Tools/inductive_set_package.ML

       end) fs
   in
     thm |>
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (HOL_basic_ss addsimps to_set_simps
-        addsimprocs [strong_ind_simproc pred_arities]) |>
+        addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
     RuleCases.save thm
   end;
 
 val to_set_att = Thm.rule_attribute o to_set;