--- a/Nominal/Fv.thy	Wed Mar 17 12:23:04 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 17:09:01 2010 +0100
@@ -591,7 +591,7 @@
   split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
   THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
-       add_0_left supp_zero_perm Int_empty_left})
+       add_0_left supp_zero_perm Int_empty_left split_conv})
 *}