--- a/Quot/Nominal/Nominal2_Eqvt.thy	Wed Feb 03 17:36:25 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Thu Feb 04 14:55:21 2010 +0100
@@ -11,6 +11,7 @@
 
 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 ..
@@ -233,6 +234,7 @@
 
   (* nominal *)
   permute_eqvt supp_eqvt fresh_eqvt
+  permute_pure
 
   (* datatypes *)
   permute_prod.simps
@@ -242,9 +244,8 @@
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
   Diff_eqvt Compl_eqvt insert_eqvt
 
-declare permute_pure [eqvt]
-
-(* thm eqvts *)
+thm eqvts
+thm eqvts_raw
 
 text {* helper lemmas for the eqvt_tac *}