--- a/FSet.thy	Fri Dec 04 14:11:03 2009 +0100
+++ b/FSet.thy	Fri Dec 04 14:11:20 2009 +0100
@@ -337,8 +337,6 @@
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done
 
-lemma cheat: "P" sorry
-
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})

--- a/QuotMain.thy	Fri Dec 04 14:11:03 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 14:11:20 2009 +0100
@@ -146,7 +146,7 @@
 declare [[map "fun" = (fun_map, FUN_REL)]]
 
 lemmas [quotient_thm] = 
-  FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT
+  FUN_QUOTIENT LIST_QUOTIENT
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}