--- a/src/HOL/Library/Permutation.thy Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Library/Permutation.thy Thu Aug 07 12:17:41 2014 +0200
@@ -162,7 +162,7 @@
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