diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -801,7 +801,7 @@
 apply(blast)+
 done
 
-lemma Abs1_eq_fresh:
+lemma Abs1_eq_iff_fresh:
   fixes x y::"'a::fs"
   and a b c::"'b::at"
   assumes "atom c \<sharp> (a, b, x, y)"
@@ -843,7 +843,7 @@
     by (simp add: Abs1_eq)
 qed
 
-lemma Abs1_eq_all:
+lemma Abs1_eq_iff_all:
   fixes x y::"'a::fs"
   and z::"'c::fs"
   and a b::"'b::at"
@@ -852,25 +852,25 @@
   and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
 apply -
 apply(auto) 
-apply(simp add: Abs1_eq_fresh(1)[symmetric])
+apply(simp add: Abs1_eq_iff_fresh(1)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
-apply(subst Abs1_eq_fresh(1))
+apply(subst Abs1_eq_iff_fresh(1))
 apply(auto simp add: fresh_Pair)[1]
 apply(assumption)
-apply(simp add: Abs1_eq_fresh(2)[symmetric])
+apply(simp add: Abs1_eq_iff_fresh(2)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
-apply(subst Abs1_eq_fresh(2))
+apply(subst Abs1_eq_iff_fresh(2))
 apply(auto simp add: fresh_Pair)[1]
 apply(assumption)
-apply(simp add: Abs1_eq_fresh(3)[symmetric])
+apply(simp add: Abs1_eq_iff_fresh(3)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
-apply(subst Abs1_eq_fresh(3))
+apply(subst Abs1_eq_iff_fresh(3))
 apply(auto simp add: fresh_Pair)[1]
 apply(assumption)
 done
@@ -964,6 +964,35 @@
 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)
 
 
+ML {*
+fun alpha_single_simproc thm _ ss ctrm =
+ let
+    val ctxt = Simplifier.the_context ss
+    val thy = Proof_Context.theory_of ctxt
+    val _ $ (_ $ x) $ (_ $ y) = term_of ctrm
+    val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y [])
+      |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs}))
+      |> map Free
+      |> HOLogic.mk_tuple
+      |> Thm.cterm_of thy
+    val cvrs_ty = ctyp_of_term cvrs
+    val thm' = thm
+      |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] 
+  in
+    SOME thm'
+  end
+*}
+
+simproc_setup alpha_set ("[{atom a}]set. x = [{atom b}]set. y") = 
+  {* alpha_single_simproc @{thm Abs1_eq_iff_all(1)[THEN eq_reflection]} *}
+
+simproc_setup alpha_res ("[{atom a}]res. x = [{atom b}]res. y") = 
+  {* alpha_single_simproc @{thm Abs1_eq_iff_all(2)[THEN eq_reflection]} *}
+
+simproc_setup alpha_lst ("[[atom a]]lst. x = [[atom b]]lst. y") = 
+  {* alpha_single_simproc @{thm Abs1_eq_iff_all(3)[THEN eq_reflection]} *}
+
+
 subsection {* Renaming of bodies of abstractions *}
 
 lemma Abs_rename_set: