--- a/Nominal/Ex/SingleLet.thy	Mon Aug 16 19:57:41 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 06:39:27 2010 +0800
@@ -62,11 +62,6 @@
 
 section {* NOT *} 
 
-lemma [quot_respect]:
-  "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw"
-sorry
-
-
 ML {*
  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) 
    @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps