diff -r 4135198bbb8a -r 56cebe7f8e24 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Tue Apr 13 00:47:57 2010 +0200
+++ b/Nominal/FSet.thy	Tue Apr 13 00:53:32 2010 +0200
@@ -43,8 +43,7 @@
 quotient_definition
   fin ("_ |\<in>| _" [50, 51] 50)
 where
-  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-is "memb"
+  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
 
 abbreviation
   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
@@ -63,7 +62,7 @@
   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 by simp
 
-section {* Augmenting a set -- @{const finsert} *}
+section {* Augmenting an fset -- @{const finsert} *}
 
 lemma nil_not_cons:
   shows