--- 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 *})