--- a/Nominal/Fv.thy	Sat Mar 27 09:41:00 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 09:56:35 2010 +0100
@@ -888,14 +888,32 @@
   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 *)
+ML {*
+fun choose_alpha_abs eqiff =
+let
+  fun exists_subterms f ts = true mem (map (exists_subterm f) ts);
+  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_res} then 1 else
+    if check @{const_name alpha_lst} then 2 else
+    error "Failure choosing supp_abs"
+in
+  nth @{thms supp_abs[symmetric]} no
+end
+*}
+
 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[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
-  simp_tac (HOL_basic_ss addsimps (@{thm permute_abs} :: perm)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW