diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/Ex/Finite_Alpha.thy
--- a/Nominal/Ex/Finite_Alpha.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Ex/Finite_Alpha.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -8,7 +8,12 @@
       and "p \<bullet> as = bs"
     shows "(as, x) \<approx>set (op =) supp p (bs, y)"
   using assms unfolding alphas
-  by (metis Diff_eqvt atom_set_perm_eq supp_eqvt)
+  apply(simp)
+  apply(clarify)
+  apply(simp only: Diff_eqvt[symmetric] supp_eqvt[symmetric])
+  apply(simp only: atom_set_perm_eq)
+  done
+
 
 lemma
   assumes "(supp x - set as) \<sharp>* p"
@@ -16,7 +21,11 @@
       and "p \<bullet> as = bs"
     shows "(as, x) \<approx>lst (op =) supp p (bs, y)"
   using assms unfolding alphas
-  by (metis Diff_eqvt atom_set_perm_eq supp_eqvt supp_of_atom_list)
+  apply(simp)
+  apply(clarify)
+  apply(simp only: set_eqvt[symmetric] Diff_eqvt[symmetric] supp_eqvt[symmetric])
+  apply(simp only: atom_set_perm_eq)
+  done
 
 lemma
   assumes "(supp x - as) \<sharp>* p"
@@ -32,8 +41,8 @@
   apply (rule trans)
   apply (rule supp_perm_eq[symmetric, of _ p])
   apply (simp add: supp_finite_atom_set fresh_star_def)
-  apply blast
-  apply (simp add: eqvts)
+  apply(auto)[1]
+  apply(simp only: Diff_eqvt inter_eqvt supp_eqvt)
   apply (simp add: fresh_star_def)
   apply blast
   done