--- a/Nominal/Nominal2_FSet.thy	Mon Apr 12 17:44:26 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Tue Apr 13 00:47:57 2010 +0200
@@ -18,14 +18,13 @@
 instantiation FSet.fset :: (pt) pt
 begin
 
-term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
 quotient_definition
   "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
-instance proof
+instance 
+proof
   fix x :: "'a fset" and p q :: "perm"
   show "0 \<bullet> x = x"
     by (lifting permute_zero [where 'a="'a list"])
@@ -36,17 +35,12 @@
 end
 
 lemma permute_fset[eqvt]:
-  "p \<bullet> ({||} :: 'a :: pt fset) = {||}"
+  "(p \<bullet> {||}) = ({||} :: 'a::pt fset)"
   "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
   by (lifting permute_list.simps)
 
-lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"
-  apply (induct l)
-  apply (simp_all)
-  apply (simp only: eqvt_apply)
-  done
-
-lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
+lemma fmap_eqvt[eqvt]: 
+  shows "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
   by (lifting map_eqvt)
 
 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"