# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1316538279 -7200
# Node ID b037ae269f5098c965231454815f0d23618d3678
# Parent  204a488c71c6201b335f9ebdf68845cf812e3a8d
updated to Isabelle 19 Sept

diff -r 204a488c71c6 -r b037ae269f50 Nominal/Nominal2_Base.thy
--- 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 {*