--- a/Nominal/Nominal2_Eqvt.thy	Tue Mar 02 17:11:19 2010 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Tue Mar 02 17:11:58 2010 +0100
@@ -5,7 +5,7 @@
     (Contains most, but not all such lemmas.)
 *)
 theory Nominal2_Eqvt
-imports Nominal2_Base
+imports Nominal2_Base Nominal2_Atoms
 uses ("nominal_thmdecls.ML")
      ("nominal_permeq.ML")
 begin
@@ -248,7 +248,9 @@
 
   (* sets *)
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
-  Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt
+  Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
+
+  atom_eqvt
 
 thm eqvts
 thm eqvts_raw
@@ -301,4 +303,4 @@
 oops
 
 
-end
\ No newline at end of file
+end