--- a/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 21 21:52:30 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Thu Apr 22 05:16:23 2010 +0200
@@ -6,7 +6,7 @@
     (contains many, but not all such lemmas).
 *)
 theory Nominal2_Eqvt
-imports Nominal2_Base Nominal2_Atoms
+imports Nominal2_Base 
 uses ("nominal_thmdecls.ML")
      ("nominal_permeq.ML")
      ("nominal_eqvt.ML")
@@ -259,7 +259,7 @@
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
   Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
 
-  atom_eqvt add_perm_eqvt
+  add_perm_eqvt
 
 lemmas [eqvt_raw] =
   permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *)