--- a/Nominal/Ex/Let.thy	Sat Nov 13 10:25:03 2010 +0000
+++ b/Nominal/Ex/Let.thy	Sat Nov 13 22:23:26 2010 +0000
@@ -18,8 +18,6 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
-thm permute_bn_raw.simps
-
 thm at_set_avoiding2
 thm trm_assn.fv_defs
 thm trm_assn.eq_iff 
@@ -32,11 +30,6 @@
 thm trm_assn.fresh
 thm trm_assn.exhaust[where y="t", no_vars]
 
-quotient_definition
-  "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"
-is
-  "permute_bn_raw"
-
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
 
 lemma uu: