--- a/Nominal/Fv.thy	Fri Mar 19 12:28:35 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 19 14:54:30 2010 +0100
@@ -908,7 +908,7 @@
 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 supp_atom_image supp_fset_to_set
-    supp_fmap_atom finite_insert finite.emptyI finite_Un})
+    supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
 *}
 
 ML {*