--- a/Quot/Nominal/Nominal2_Eqvt.thy	Sat Feb 06 12:58:56 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Sun Feb 07 10:16:21 2010 +0100
@@ -226,8 +226,6 @@
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 
-
-
 lemmas [eqvt] = 
   (* connectives *)
   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
@@ -235,7 +233,8 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  supp_eqvt fresh_eqvt permute_pure
+  permute_eqvt supp_eqvt fresh_eqvt
+  permute_pure
 
   (* datatypes *)
   permute_prod.simps
@@ -245,8 +244,6 @@
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
   Diff_eqvt Compl_eqvt insert_eqvt
 
-lemmas [eqvt_raw] = permute_eqvt
-
 thm eqvts
 thm eqvts_raw