--- a/Nominal/Nominal2_Abs.thy	Thu Sep 08 11:21:03 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy	Thu Sep 08 13:03:19 2011 +0100
@@ -64,7 +64,9 @@
   unfolding set_eqvt[symmetric]
   unfolding permute_fun_app_eq[symmetric]
   unfolding Diff_eqvt[symmetric]
-  by (auto simp add: permute_bool_def fresh_star_permute_iff)
+  unfolding eq_eqvt[symmetric]
+  unfolding fresh_star_eqvt[symmetric]
+  by (auto simp add: permute_bool_def)
 
 
 section {* Equivalence *}