--- a/Nominal/Fv.thy	Fri Mar 26 16:46:40 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 26 17:01:22 2010 +0100
@@ -872,7 +872,7 @@
 *}
 
 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 (simp add: supp_abs supp_Pair)
   apply blast
   done
 
@@ -880,10 +880,10 @@
 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 @{thms supp_abs[symmetric]}) 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 (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW