--- a/Quot/Nominal/Nominal2_Eqvt.thy	Thu Feb 04 17:39:04 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Fri Feb 05 09:06:27 2010 +0100
@@ -226,6 +226,8 @@
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 
+
+
 lemmas [eqvt] = 
   (* connectives *)
   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
@@ -233,8 +235,7 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  permute_eqvt supp_eqvt fresh_eqvt
-  permute_pure
+  supp_eqvt fresh_eqvt permute_pure
 
   (* datatypes *)
   permute_prod.simps
@@ -244,6 +245,8 @@
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
   Diff_eqvt Compl_eqvt insert_eqvt
 
+lemmas [eqvt_raw] = permute_eqvt
+
 thm eqvts
 thm eqvts_raw