diff -r ae860c95bf9f -r 69780ae147f5 Nominal/Ex/Let.thy --- 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