--- 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