--- a/Nominal/Nominal2_Abs.thy	Mon Sep 19 21:52:59 2011 +0200
+++ b/Nominal/Nominal2_Abs.thy	Tue Sep 20 14:44:50 2011 +0900
@@ -509,16 +509,13 @@
     (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)"
   by (lifting alphas_abs_stronger)
 
+lemma alpha_res_alpha_set:
+  "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
+  using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
+
 lemma Abs_eq_res_set:
   "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))"
-  unfolding Abs_eq_iff
-  using alpha_abs_set_abs_res alpha_abs_res_abs_set
-  apply auto
-  apply (rule_tac x="p" in exI)
-  apply assumption
-  apply (rule_tac x="p" in exI)
-  apply assumption
-  done
+  unfolding Abs_eq_iff alpha_res_alpha_set by rule
 
 lemma Abs_eq_res_supp:
   assumes asm: "supp x \<subseteq> bs"