--- a/Nominal/FSet.thy	Fri Oct 15 16:32:34 2010 +0900
+++ b/Nominal/FSet.thy	Fri Oct 15 13:28:39 2010 +0100
@@ -160,7 +160,7 @@
   by (induct ys arbitrary: xs) (auto)
 
 
-text {* Respectfullness *}
+text {* Respectfulness *}
 
 lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
@@ -299,7 +299,7 @@
 qed
 
 lemma [quot_respect]:
-  shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
   by auto
 
 text {* Distributive lattice with bot *}