diff -r bcf48a1cb24b -r 177a32a4f289 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Jun 09 11:10:41 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 09 15:03:58 2011 +0900
@@ -273,7 +273,7 @@
 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa")
 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya")
 apply(simp add: eqvt_at_def)
-apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+
+apply(simp_all add: swap_fresh_fresh)
 done
 
 termination