--- a/Nominal/Ex/Let.thy	Wed Jul 06 15:59:11 2011 +0200
+++ b/Nominal/Ex/Let.thy	Wed Jul 06 23:11:30 2011 +0200
@@ -31,6 +31,7 @@
 thm trm_assn.bn_defs
 thm trm_assn.bn_inducts
 thm trm_assn.perm_simps
+thm trm_assn.permute_bn
 thm trm_assn.induct
 thm trm_assn.inducts
 thm trm_assn.distinct