--- a/Nominal/Ex/ExPS8.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExPS8.thy	Sun May 09 12:26:10 2010 +0100
@@ -48,6 +48,11 @@
 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
 
+
+declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
 end