diff -r 219e3ff68de8 -r fd483d8f486b Nominal/LFex.thy
--- a/Nominal/LFex.thy	Thu Mar 18 07:35:44 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 07:43:44 2010 +0100
@@ -46,7 +46,7 @@
   "supp (App M N) = supp M \<union> supp N"
   "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
   apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm)
-  apply(simp_all only: kind_ty_trm_inject Abs_eq_iff alpha_gen)
+  apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen)
   apply(simp_all only: ex_out)
   apply(simp_all only: eqvts[symmetric])
   apply(simp_all only: Collect_neg_conj)