# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307599438 -32400
# Node ID 177a32a4f289945e311f48f060ca84731132cd81
# Parent  bcf48a1cb24b01b807172b2cdd0810a536c2fa2d
Minor simplification

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