--- a/Nominal/FSet.thy	Sun Oct 17 15:53:37 2010 +0100
+++ b/Nominal/FSet.thy	Sun Oct 17 21:40:23 2010 +0100
@@ -9,7 +9,7 @@
 imports Quotient_List
 begin
 
-text {* Definiton of the equivalence relation over lists *}
+text {* Definition of the equivalence relation over lists *}
 
 fun
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
@@ -523,9 +523,9 @@
 subsection {* fset *}
 
 lemma fset_simps [simp]:
-  "fset {||} = ({} :: 'a set)"
-  "fset (insert_fset (x :: 'a) S) = insert x (fset S)"
-  by (lifting set.simps)
+  shows "fset {||} = {}"
+  and   "fset (insert_fset x S) = insert x (fset S)"
+  by (descending, simp)+
 
 lemma finite_fset [simp]: 
   shows "finite (fset S)"