--- a/Nominal/Nominal2_Base.thy	Tue Sep 20 09:17:29 2011 +0200
+++ b/Nominal/Nominal2_Base.thy	Tue Sep 20 19:04:39 2011 +0200
@@ -953,12 +953,11 @@
   unfolding Inter_eq 
   by (perm_simp) (rule refl)
 
-
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
 unfolding Sigma_def
-unfolding UNION_eq_Union_image
+unfolding SUP_def
 by (perm_simp) (rule refl)
 
 text {*