--- a/Nominal-General/Nominal2_Base.thy	Sun May 02 21:15:52 2010 +0100
+++ b/Nominal-General/Nominal2_Base.thy	Mon May 03 00:00:33 2010 +0100
@@ -1199,8 +1199,7 @@
   assumes a: "finite S"
   shows "supp S = atom ` S"
 proof -
-  have fin: "finite (atom ` S)" 
-    using a by (simp add: finite_imageI) 
+  have fin: "finite (atom ` S)" using a by simp
   have "supp S = supp (atom ` S)" by (rule atom_image_supp)
   also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)
   finally show "supp S = atom ` S" by simp