diff -r 843e0a2d44d7 -r db218886e674 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Thu May 06 14:10:26 2010 +0200
+++ b/Nominal/Rsp.thy	Thu May 06 14:10:56 2010 +0200
@@ -63,7 +63,7 @@
   rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ fvbv_simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
   TRY o blast_tac (claset_of ctxt)
@@ -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 split_conv 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 prod_rel.simps prod_fv.simps}))
   ))
 *}