--- a/Nominal/Ex/ExLetRec.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExLetRec.thy	Sun May 09 12:26:10 2010 +0100
@@ -30,6 +30,11 @@
 thm trm_lts.supp
 thm trm_lts.fv[simplified trm_lts.supp]
 
+declare permute_trm_raw_permute_lts_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
 (* why is this not in HOL simpset? *)
 lemma set_sub: "{a, b} - {b} = {a} - {b}"
 by auto