--- a/Nominal/Ex/ExLet.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExLet.thy	Sun May 09 12:26:10 2010 +0100
@@ -35,6 +35,13 @@
 thm trm_lts.fv[simplified trm_lts.supp(1-2)]
 
 
+declare permute_trm_raw_permute_lts_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+
 primrec
   permute_bn_raw
 where
@@ -95,14 +102,14 @@
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
   apply (simp add: perm_bn[symmetric])
-  apply (simp add: eqvts[symmetric])
-  apply (simp add: supp_abs)
+  apply(rule conjI)
+  apply(drule supp_perm_eq)
+  apply(simp add: abs_eq_iff)
+  apply(simp add: alphas_abs alphas)
+  apply(drule conjunct1)
   apply (simp add: trm_lts.supp)
-  apply (rule supp_perm_eq[symmetric])
-  apply (subst supp_finite_atom_set)
-  apply (rule finite_Diff)
-  apply (simp add: finite_supp)
-  apply (assumption)
+  apply(simp add: supp_abs)
+  apply (simp add: trm_lts.supp)
   done