src/HOL/Library/Permutation.thy

 lemma eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys"
   apply (induct xs arbitrary: ys rule: length_induct)
   apply (case_tac "remdups xs")
    apply simp_all
   apply (subgoal_tac "a \<in> set (remdups ys)")
-   prefer 2 apply (metis set_simps(2) insert_iff set_remdups)
+   prefer 2 apply (metis list.set(2) insert_iff set_remdups)
   apply (drule split_list) apply (elim exE conjE)
   apply (drule_tac x = list in spec) apply (erule impE) prefer 2
    apply (drule_tac x = "ysa @ zs" in spec) apply (erule impE) prefer 2
     apply simp
     apply (subgoal_tac "a # list <~~> a # ysa @ zs")