--- a/Nominal/TySch.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -22,39 +22,7 @@
 thm t_tyS.distinct
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 
-lemma finite_fv_t_tyS:
-  shows "finite (fv_t t)" "finite (fv_tyS ts)"
-  by (induct rule: t_tyS.inducts) (simp_all)
-
-lemma supp_fv_t_tyS:
-  shows "fv_t t = supp t" "fv_tyS ts = supp ts"
-  apply(induct rule: t_tyS.inducts)
-  apply(simp_all only: t_tyS.fv)
-  prefer 3
-  apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
-  prefer 2
-  apply(subst finite_supp_Abs)
-  apply(drule sym)
-  apply(simp add: finite_fv_t_tyS(1))
-  apply(simp)
-  apply(simp_all (no_asm) only: supp_def)
-  apply(simp_all only: t_tyS.perm)
-  apply(simp_all only: permute_ABS)
-  apply(simp_all only: t_tyS.eq_iff Abs_eq_iff)
-  apply(simp_all only: alpha_gen)
-  apply(simp_all only: eqvts[symmetric])
-  apply(simp_all only: eqvts eqvts_raw)
-  apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
-  apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
-  apply(simp_all only: de_Morgan_conj[symmetric])
-  done
-
-instance t and tyS :: fs
-  apply default
-  apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS)
-  done
-
-lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS]
+lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
 
 lemma induct:
   assumes a1: "\<And>name b. P b (Var name)"