--- a/Nominal/Fv.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -891,13 +891,9 @@
 end
 *}
 
-lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
-  apply (simp add: supp_abs supp_Pair)
-  apply blast
-  done
-
 (* TODO: this is a hack, it assumes that only one type of Abs's is present
-   in the type and chooses this supp_abs *)
+   in the type and chooses this supp_abs. Additionally single atoms are
+   treated properly. *)
 ML {*
 fun choose_alpha_abs eqiff =
 let
@@ -905,19 +901,31 @@
   val terms = map prop_of eqiff;
   fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
   val no =
-    if check @{const_name alpha_gen} then 0 else
+    if check @{const_name alpha_lst} then 2 else
     if check @{const_name alpha_res} then 1 else
-    if check @{const_name alpha_lst} then 2 else
+    if check @{const_name alpha_gen} then 0 else
     error "Failure choosing supp_abs"
 in
   nth @{thms supp_abs[symmetric]} no
 end
 *}
+lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"
+by (rule supp_abs(1))
+
+lemma supp_abs_sum:
+  "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+  "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
+  "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"
+  apply (simp_all add: supp_abs supp_Pair)
+  apply blast+
+  done
+
 
 ML {*
 fun supp_eq_tac ind fv perm eqiff ctxt =
   rel_indtac ind THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW