--- a/src/HOL/Library/Permutation.thy Wed Feb 19 22:02:23 2014 +1100
+++ b/src/HOL/Library/Permutation.thy Wed Feb 19 16:32:37 2014 +0100
@@ -157,7 +157,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 set_simps(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