--- a/Nominal/FSet.thy	Tue Apr 20 15:59:57 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 09:13:32 2010 +0200
@@ -563,10 +563,6 @@
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
   is "ffold_raw"
 
-lemma funion_sym_pre:
-  "xs @ ys \<approx> ys @ xs"
-  by auto
-
 lemma set_cong: 
   shows "(set x = set y) = (x \<approx> y)"
   by auto
@@ -760,13 +756,9 @@
   shows "S |\<union>| {||} = S"
   by (lifting append_Nil2)
 
-lemma funion_sym:
-  shows "S |\<union>| T = T |\<union>| S"
-  by (lifting funion_sym_pre)
+thm sup.commute[where 'a="'a fset"]
 
-lemma funion_assoc:
-  shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
-  by (lifting append_assoc)
+thm sup.assoc[where 'a="'a fset"]
 
 lemma singleton_union_left:
   "{|a|} |\<union>| S = finsert a S"
@@ -774,7 +766,7 @@
 
 lemma singleton_union_right:
   "S |\<union>| {|a|} = finsert a S"
-  by (subst funion_sym) simp
+  by (subst sup.commute) simp
 
 section {* Induction and Cases rules for finite sets *}