--- a/Nominal/Rsp.thy	Sat Mar 20 08:56:07 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 20 09:27:28 2010 +0100
@@ -95,18 +95,15 @@
 *}
 
 ML {*
-fun constr_rsp_tac inj rsp equivps =
-let
-  val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
-in
+fun constr_rsp_tac inj rsp =
   REPEAT o rtac impI THEN'
   simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
-   rtac @{thm exI[of _ "0 :: perm"]} THEN'
-   asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
+   REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
+   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+   asm_full_simp_tac (HOL_ss addsimps (rsp @
+     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
   ))
-end
 *}
 
 (* Testing code