diff -r f970ca9b5bec -r 4908db645f98 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 17 20:42:22 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 20:42:42 2010 +0100
@@ -609,10 +609,8 @@
   THEN_ALL_NEW
   split_conjs THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
-  (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [
-    (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})),
-    (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
-  ])
+  TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
+  (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
 *}
 
 ML {*