--- a/Nominal/Nominal2_FSet.thy	Fri Oct 15 15:47:20 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Fri Oct 15 15:56:16 2010 +0100
@@ -4,14 +4,9 @@
         FSet 
 begin
 
-lemma permute_rsp_fset[quot_respect]:
+lemma permute_fset_rsp[quot_respect]:
   shows "(op = ===> list_eq ===> list_eq) permute permute"
-  apply(simp)
-  apply(clarify)
-  apply(rule_tac p="-x" in permute_boolE)
-  apply(perm_simp add: permute_minus_cancel)
-  apply(simp)
-  done
+  by (simp add: set_eqvt[symmetric])
 
 instantiation fset :: (pt) pt
 begin
@@ -33,7 +28,7 @@
 lemma permute_fset[simp, eqvt]:
   fixes S::"('a::pt) fset"
   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
-  and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
+  and   "(p \<bullet> finsert x S) = finsert (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
 lemma fmap_eqvt[eqvt]: 
@@ -44,33 +39,35 @@
   shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
   by (lifting set_eqvt)
 
-lemma supp_fset:
+lemma supp_fset [simp]:
   shows "supp (fset S) = supp S"
   unfolding supp_def
   by (perm_simp) (simp add: fset_cong)
 
-lemma supp_fempty:
+lemma supp_fempty [simp]:
   shows "supp {||} = {}"
   unfolding supp_def
   by simp
 
-lemma supp_finsert:
+lemma supp_finsert [simp]:
   fixes x::"'a::fs"
   and   S::"'a fset"
   shows "supp (finsert x S) = supp x \<union> supp S"
   apply(subst supp_fset[symmetric])
-  apply(simp add: supp_fset)
-  apply(simp add: supp_of_fin_insert)
-  apply(simp add: supp_fset)
+  apply(simp add: supp_fset supp_of_fin_insert)
   done
 
+lemma fset_finite_supp:
+  fixes S::"('a::fs) fset"
+  shows "finite (supp S)"
+  by (induct S) (simp_all add: finite_supp)
+
+
+subsection {* finite sets are fs-types *}
 
 instance fset :: (fs) fs
   apply (default)
-  apply (induct_tac x rule: fset_induct)
-  apply (simp add: supp_fempty)
-  apply (simp add: supp_finsert)
-  apply (simp add: finite_supp)
+  apply (rule fset_finite_supp)
   done
 
 lemma atom_fmap_cong: