diff -r d3101a5b9c4d -r c28403308b34 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Tue Mar 02 13:28:54 2010 +0100
+++ b/Nominal/Rsp.thy	Tue Mar 02 14:24:57 2010 +0100
@@ -78,8 +78,12 @@
 ML {*
 fun fvbv_rsp_tac induct fvbv_simps =
   ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-  (TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac
-  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))
+  (TRY o rtac @{thm TrueI})) THEN_ALL_NEW
+  asm_full_simp_tac
+  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))
+  THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN'
+  asm_full_simp_tac
+  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))))
 *}
 
 ML {*
@@ -158,7 +162,7 @@
   (
    (asm_full_simp_tac (HOL_ss addsimps 
       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-    THEN_ALL_NEW (etac @{thm exi[of _ _ "p"]} THEN'
+    THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN'
       REPEAT o etac conjE THEN'
       (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW
       (asm_full_simp_tac HOL_ss) THEN_ALL_NEW