--- a/Nominal/ExTySch.thy	Sat Mar 27 09:41:00 2010 +0100
+++ b/Nominal/ExTySch.thy	Sat Mar 27 09:56:35 2010 +0100
@@ -12,23 +12,7 @@
 and tyS =
   All xs::"name fset" ty::"t" bind xs in ty
 
-lemma t_tyS_supp_fv: "fv_t t = supp t \<and> fv_tyS tyS = supp tyS"
-apply (induct rule: t_tyS.induct)
-apply (simp_all only: t_tyS.fv)
-apply (simp_all only: supp_abs(2)[symmetric])
-apply(simp_all (no_asm) only: supp_def)
-apply(simp_all only: t_tyS.perm permute_abs)
-apply(simp only: t_tyS.eq_iff supp_at_base[simplified supp_def])
-apply(simp only: t_tyS.eq_iff Collect_disj_eq[symmetric] infinite_Un[symmetric])
-apply simp
-apply(simp only: Abs_eq_iff t_tyS.eq_iff)
-apply (simp add: alphas)
-apply (simp add: eqvts[symmetric])
-apply (simp add: eqvts eqvts_raw)
-done
-
-lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS_supp_fv]
-
+lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
 
 lemma size_eqvt_raw:
   "size (pi \<bullet> t :: t_raw) = size t"