diff -r a0134252ac29 -r a879f14b6f95 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Wed Feb 19 22:02:23 2014 +1100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Wed Feb 19 16:32:37 2014 +0100
@@ -985,7 +985,7 @@
   have b: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
   have c: "xs = [] \<Longrightarrow> thesis" using b 
     apply(simp)
-    by (metis List.set.simps(1) emptyE empty_subsetI)
+    by (metis List.set_simps(1) emptyE empty_subsetI)
   have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
   proof -
     fix x :: 'a