diff -r c0ab7451b20d -r 751d1349329b Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Rsp.thy	Mon May 10 15:45:04 2010 +0200
@@ -101,7 +101,7 @@
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps 
-    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW
+    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW
   (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
   THEN_ALL_NEW