--- a/Nominal/Ex/Let.thy	Wed Oct 06 08:13:09 2010 +0100
+++ b/Nominal/Ex/Let.thy	Wed Oct 06 21:32:44 2010 +0100
@@ -28,7 +28,7 @@
 thm trm_assn.distinct
 thm trm_assn.supp
 thm trm_assn.fresh
-thm trm_assn.exhaust
+thm trm_assn.exhaust[where y="t", no_vars]
 
 primrec
   permute_bn_raw