diff -r d3101a5b9c4d -r c28403308b34 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 02 13:28:54 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 02 14:24:57 2010 +0100
@@ -325,7 +325,7 @@
 fun symp_tac induct inj eqvt =
   (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
-  (etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN'
+  (REPEAT o etac conjE THEN' etac @{thm exi_neg} 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
   (etac @{thm alpha_gen_compose_sym} THEN' 
@@ -367,7 +367,7 @@
   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
   (
     asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct)
-    THEN_ALL_NEW (etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW
+    THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW
     (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
     (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW