--- a/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Fri Jul 22 11:37:16 2011 +0100
@@ -288,26 +288,6 @@
 
 termination (eqvt) by lexicographic_order
 
-thm subst_substs.eqvt[no_vars]
-thm subst_def
-thm substs_def
-thm Sum_Type.Projr.simps
-
-lemma
- shows "(p \<bullet> subst x y) = subst (p \<bullet> x) (p \<bullet> y)"
- and   "(p \<bullet> substs x' y') = substs (p \<bullet> x') (p \<bullet> y')"
-unfolding subst_def substs_def
-thm permute_fun_app_eq
-thm Sum_Type.Projl_def sum_rec_def
-apply(simp add: permute_fun_def)
-unfolding subst_substs_sumC_def
-thm subst_substs.eqvt
-apply(case_tac x)
-apply(simp)
-apply(case_tac a)
-apply(simp)
-thm subst_def
-apply(simp)
 
 section {* defined as two separate nominal datatypes *}
 
@@ -383,17 +363,24 @@
   apply (rule, perm_simp, rule)
   apply auto[2]
   apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
-  apply auto
+  apply auto[1]
+  apply(simp)
+  apply(erule conjE)
   apply (erule Abs_res_fcb)
   apply (simp add: Abs_fresh_iff)
-  apply (simp add: Abs_fresh_iff)
-  apply auto[1]
-  apply (simp add: fresh_def fresh_star_def)
-  apply (rule contra_subsetD[OF  supp_subst])
-  apply simp
-  apply blast
+  apply(simp add: fresh_def)
+  apply(simp add: supp_Abs)
+  apply(rule impI)
+  apply(subgoal_tac "x \<notin> supp \<theta>")
+  prefer 2
+  apply(auto simp add: fresh_star_def fresh_def)[1]
+  apply(subgoal_tac "x \<in> supp t")
+  using supp_subst
+  apply(blast)
+  using supp_subst
+  apply(blast)
   apply clarify
-  apply (simp add: subst_eqvt)
+  apply (simp add: subst2.eqvt)
   apply (subst Abs_eq_iff)
   apply (rule_tac x="0::perm" in exI)
   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
@@ -415,7 +402,6 @@
   apply blast
   done
 
-
 text {* Some Tests about Alpha-Equality *}
 
 lemma