diff -r a4743b7cd887 -r f65564bcf342 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Sat Mar 20 16:27:51 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 20 18:16:26 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