--- a/Nominal/Nominal2_Base.thy	Mon Aug 06 13:50:19 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Aug 07 16:55:17 2012 +0100
@@ -1046,9 +1046,6 @@
   apply(simp)
   done
 
-thm eqvts_raw
-
-
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
@@ -1131,8 +1128,12 @@
 lemma fun_upd_eqvt[eqvt]:
   shows "p \<bullet> (f(x := y)) = (p \<bullet> f)((p \<bullet> x) := (p \<bullet> y))"
 unfolding fun_upd_def
-by (simp)
-
+by simp
+
+lemma comp_eqvt [eqvt]:
+  shows "p \<bullet> (f \<circ> g) = (p \<bullet> f) \<circ> (p \<bullet> g)"
+unfolding comp_def
+by simp
 
 subsubsection {* Equivariance for product operations *}