diff -r 2b0cc308fd6a -r 9eab1dfc14d2 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Apr 21 21:52:30 2010 +0200
+++ b/Nominal/Abs.thy	Thu Apr 22 05:16:23 2010 +0200
@@ -2,8 +2,8 @@
 imports "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Nominal2_FSet"
         "Quotient" 
+        "Quotient_List"
         "Quotient_Product" 
 begin
 
@@ -397,13 +397,12 @@
 
 section {* BELOW is stuff that may or may not be needed *}
 
-
 lemma supp_atom_image:
   fixes as::"'a::at_base set"
   shows "supp (atom ` as) = supp as"
 apply(simp add: supp_def)
 apply(simp add: image_eqvt)
-apply(simp add: atom_eqvt_raw)
+apply(simp add: eqvts_raw)
 apply(simp add: atom_image_cong)
 done