--- a/Nominal/Ex/TypeSchemes.thy	Thu Feb 17 12:01:08 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Feb 17 17:02:25 2011 +0900
@@ -63,6 +63,14 @@
 apply(simp)
 done
 
+lemma helper:
+  assumes "A - C = A - D"
+  and "B - C = B - D"
+  and "E \<subseteq> A \<union> B"
+  shows "E - C = E - D"
+using assms
+by blast
+
 nominal_primrec
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
@@ -224,7 +232,7 @@
 defer
 apply (simp add: ty_tys.eq_iff)
 apply (simp only: Abs_eq_res_set)
-apply (subgoal_tac "(atom ` fset xsa \<inter> supp T - atom ` fset xs \<inter> supp Ta) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
+apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
 apply (subst (asm) Abs_eq_iff2)
 apply (clarify)
 apply (simp add: alphas)
@@ -260,11 +268,7 @@
 apply (simp add: supp_Pair finite_supp)
 apply (simp add: fresh_Pair)
 apply(auto simp add: Abs_fresh_iff fresh_star_def)[1]
-prefer 2
 apply auto[1]
-apply (erule_tac x="atom x" in ballE)
-apply auto[1]
-apply (auto simp add: fresh_def)[1]
 
 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
 prefer 2
@@ -275,12 +279,25 @@
 apply blast
 apply(simp add: eqvt_at_def inter_eqvt supp_eqvt)
 apply (simp only: Abs_eq_res_set[symmetric])
-
-apply (rule_tac s="[p \<bullet> atom ` fset xs \<inter> supp (\<theta>', p \<bullet> T)]res. subst \<theta>' (p \<bullet> T)" in trans)
---"What if (p \<bullet> xs) is not fresh for \<theta>' ?"
+apply (simp add: Abs_eq_iff alphas)
+apply rule
+prefer 2
+apply (rule_tac x="0 :: perm" in exI)
+apply (simp add: fresh_star_zero)
+apply (rule helper)
+prefer 3
+apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)")
+apply simp
+apply (subst supp_Pair[symmetric])
+apply (rule supp_eqvt_at)
+apply (simp add: eqvt_at_def)
+defer --"because eqvt_at Ta"
+apply (simp add: supp_Pair finite_supp)
+prefer 2 apply blast
+prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI)
+--"p and xs and xsa are fresh for theta"
 oops
 
-
 section {* defined as two separate nominal datatypes *}
 
 nominal_datatype ty2 =