diff -r b41de1879dae -r 7a9217a7f681 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 11 19:43:50 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 20:49:31 2010 +0100
@@ -714,7 +714,7 @@
   simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
     REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'
     asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
-      swap_fresh_fresh fresh_atom swap_at_base_simps(3)}))
+      swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh}))
 *}
 
 ML {*
@@ -766,7 +766,7 @@
 ML {*
 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW (
   rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom finite_insert finite.emptyI finite_Un})
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image finite_insert finite.emptyI finite_Un})
 *}
 
 ML {*