--- a/Nominal/Nominal2_Eqvt.thy	Thu Mar 11 10:22:24 2010 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Thu Mar 11 15:10:07 2010 +0100
@@ -12,7 +12,6 @@
 
 section {* Logical Operators *}
 
-
 lemma eq_eqvt:
   shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
   unfolding permute_eq_iff permute_bool_def ..
@@ -214,7 +213,6 @@
   "p \<bullet> (snd x) = snd (p \<bullet> x)"
  by (cases x) simp
 
-
 section {* Units *}
 
 lemma supp_unit:
@@ -245,7 +243,7 @@
 
   (* datatypes *)
   permute_prod.simps append_eqvt rev_eqvt set_eqvt
-  fst_eqvt snd_eqvt
+  fst_eqvt snd_eqvt Pair_eqvt
 
   (* sets *)
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt