--- a/LMCS-Paper/Paper.thy	Mon Sep 19 21:52:59 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Tue Sep 20 14:44:50 2011 +0900
@@ -2414,7 +2414,7 @@
   Another technique for representing binding is higher-order abstract syntax
   (HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}. 
   This representation technique supports very elegantly many aspects of
-  \emph{single} binding, and impressive work by Lee et al ~\cite{LeeCraryHarper07} 
+  \emph{single} binding, and impressive work by Lee et al~\cite{LeeCraryHarper07} 
   has been done that uses HOAS for mechanising the metatheory of SML. We
   are, however, not aware how multiple binders of SML are represented in this
   work. Judging from the submitted Twelf-solution for the POPLmark challenge,

--- 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"