--- a/Nominal/Nominal2_Base.thy	Tue May 01 12:16:04 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Sat May 12 20:54:00 2012 +0100
@@ -405,6 +405,9 @@
   shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)"
   unfolding permute_fun_def by simp
 
+lemma permute_fun_comp:
+  shows "p \<bullet> f  = (permute p) o f o (permute (-p))"
+by (simp add: comp_def permute_fun_def)
 
 subsection {* Permutations for booleans *}