diff -r e903c32ec24f -r 693562f03eee Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Wed Oct 13 22:55:58 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Thu Oct 14 04:14:22 2010 +0100
@@ -24,10 +24,8 @@
 instance 
 proof
   fix x :: "'a fset" and p q :: "perm"
-  show "0 \<bullet> x = x"
-    by (lifting permute_zero [where 'a="'a list"])
-  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x"
-    by (lifting permute_plus [where 'a="'a list"])
+  show "0 \<bullet> x = x" by (descending) (simp)
+  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
 qed
 
 end
@@ -42,16 +40,12 @@
   shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
 
-lemma fset_to_set_eqvt [eqvt]: 
-  shows "p \<bullet> (fset_to_set S) = fset_to_set (p \<bullet> S)"
+lemma fset_eqvt[eqvt]: 
+  shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
   by (lifting set_eqvt)
 
-lemma fin_fset_to_set[simp]:
-  shows "finite (fset_to_set S)"
-  by (induct S) (simp_all)
-
-lemma supp_fset_to_set:
-  shows "supp (fset_to_set S) = supp S"
+lemma supp_fset:
+  shows "supp (fset S) = supp S"
   unfolding supp_def
   by (perm_simp) (simp add: fset_cong)
 
@@ -62,11 +56,12 @@
 
 lemma supp_finsert:
   fixes x::"'a::fs"
+  and   S::"'a fset"
   shows "supp (finsert x S) = supp x \<union> supp S"
-  apply(subst supp_fset_to_set[symmetric])
-  apply(simp add: supp_fset_to_set)
+  apply(subst supp_fset[symmetric])
+  apply(simp add: supp_fset)
   apply(simp add: supp_of_fin_insert)
-  apply(simp add: supp_fset_to_set)
+  apply(simp add: supp_fset)
   done
 
 
@@ -93,7 +88,7 @@
 
 lemma supp_at_fset:
   fixes S::"('a::at_base) fset"
-  shows "supp S = fset_to_set (fmap atom S)"
+  shows "supp S = fset (fmap atom S)"
   apply (induct S)
   apply (simp add: supp_fempty)
   apply (simp add: supp_finsert)
@@ -102,7 +97,7 @@
 
 lemma fresh_star_atom:
   fixes a::"'a::at_base"
-  shows "fset_to_set S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset_to_set S"
+  shows "fset S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset S"
   apply (induct S)
   apply (simp add: fresh_set_empty)
   apply simp