diff -r a9cb6a51efc3 -r be911e869fde Nominal/LFex.thy
--- a/Nominal/LFex.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -45,7 +45,7 @@
   "supp (Var x) = {atom x}"
   "supp (App M N) = supp M \<union> supp N"
   "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)"
-  apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm)
+  apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt)
   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])
@@ -58,7 +58,7 @@
 lemma supp_fv:
   "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"
   apply(induct rule: kind_ty_trm_induct)
-  apply(simp_all (no_asm) only: supp_eqs kind_ty_trm_fv)
+  apply(simp_all (no_asm) only: supp_eqs)
   apply(simp_all)
   apply(simp_all add: supp_eqs)
   apply(simp_all add: supp_Abs)
@@ -74,7 +74,7 @@
   "supp (Var x) = {atom x}"
   "supp (App M N) = supp M \<union> supp N"
   "supp (Lam A x M) = supp A \<union> (supp M - {atom x})"
-apply (simp_all add: supp_fv kind_ty_trm_fv)
+apply (simp_all add: supp_fv)
 
 end