--- a/Nominal/Rsp.thy	Thu Apr 01 08:06:01 2010 +0200
+++ b/Nominal/Rsp.thy	Thu Apr 01 08:48:33 2010 +0200
@@ -83,7 +83,7 @@
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
    simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
    asm_full_simp_tac (HOL_ss addsimps (rsp @
-     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
+     @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
   ))
 *}