--- a/Nominal/FSet.thy	Mon Oct 18 11:51:22 2010 +0100
+++ b/Nominal/FSet.thy	Mon Oct 18 12:15:44 2010 +0100
@@ -161,6 +161,8 @@
     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
   by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
 
+
+
 subsection {* Respectfulness lemmas for list operations *}
 
 lemma list_equiv_rsp [quot_respect]:
@@ -508,7 +510,7 @@
   apply simp
   done
 
-lemma [quot_respect]:
+lemma append_rsp2 [quot_respect]:
   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
 proof (intro fun_relI, elim pred_compE)
   fix x y z w x' z' y' w' :: "'a list list"
@@ -622,8 +624,6 @@
   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
   by (descending) (auto)
 
-
-(* FIXME: is this a useful lemma ? *)
 lemma in_fset_mdef:
   shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"
   by (descending) (auto)