# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272841233 -3600
# Node ID 3078fab2d7a69e5451950ca95cc1d0be71d3407f
# Parent  a48a6f88f76ed733670c1eec28eb77d448e75e81
slight tuning

diff -r a48a6f88f76e -r 3078fab2d7a6 Nominal-General/Nominal2_Base.thy
--- 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