src/HOL/List.thy

       (\<lambda>(xs, n). n#xs) ` \<Union>((\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs})"
     by (auto simp: length_Suc_conv)
   moreover
   have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
   then have "(card A - k) * \<Prod>{Suc (card A - k)..card A} = \<Prod>{Suc (card A - Suc k)..card A}"
-    by (subst setprod.insert[symmetric]) (simp add: atLeastAtMost_insertL)+
+    by (subst prod.insert[symmetric]) (simp add: atLeastAtMost_insertL)+
   ultimately show ?case
     by (simp add: card_image inj_Cons card_UN_disjoint Suc.hyps algebra_simps)
 qed
 
 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"