--- a/Nominal/FSet.thy	Sat Sep 18 05:13:42 2010 +0800
+++ b/Nominal/FSet.thy	Sat Sep 18 06:09:43 2010 +0800
@@ -634,16 +634,16 @@
 lemma insert_preserve2:
   shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
          (id ---> rep_fset ---> abs_fset) op #"
-  by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+  by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
 
 lemma [quot_preserve]:
   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id finsert_def)
 
 lemma [quot_preserve]:
   "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
 
 lemma list_all2_app_l:
@@ -858,7 +858,7 @@
 
 lemma inj_map_eq_iff:
   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
-  by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
+  by (simp add: set_eq_iff[symmetric] inj_image_eq_iff)
 
 text {* alternate formulation with a different decomposition principle
   and a proof of equivalence *}
@@ -1271,7 +1271,7 @@
 lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
   by (simp add: fminus_red)
 
-lemma expand_fset_eq:
+lemma fset_eq_iff:
   "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   by (lifting list_eq.simps[simplified memb_def[symmetric]])