--- a/Nominal/Ex/SingleLet.thy	Sat Nov 13 10:25:03 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy	Sat Nov 13 22:23:26 2010 +0000
@@ -36,22 +36,6 @@
 thm single_let.supp
 thm single_let.fresh
 
-quotient_definition
-  "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg"
-is
-  "permute_bn_raw"
-
-lemma [quot_respect]:
-  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-  apply (rule TrueI)+
-  apply simp_all
-  apply (rule_tac [!] alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-  apply simp_all
-  done
-
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
 
 lemma uu: