--- a/Nominal/FSet.thy	Wed May 26 15:35:34 2010 +0200
+++ b/Nominal/FSet.thy	Wed May 26 16:09:09 2010 +0200
@@ -160,7 +160,7 @@
 
 text {* Respectfullness *}
 
-lemma [quot_respect]:
+lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by auto
 
@@ -350,7 +350,7 @@
   then show ?thesis using f i by auto
 qed
 
-lemma [quot_respect]:
+lemma concat_rsp[quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 proof (rule fun_relI, elim pred_compE)
   fix a b ba bb