--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 01 22:55:14 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jun 02 10:11:50 2011 +0900
@@ -427,15 +427,17 @@
   apply (simp add: fresh_star_Un fresh_star_inter1)
   apply (simp add: alphas fresh_star_zero)
   apply auto[1]
+  apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
+  apply (simp add: inter_eqvt)
+  apply blast
   apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
-oops
-(*
-  apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)
+  apply (simp add: IntI image_eqI)
   apply (drule subsetD[OF supp_subst])
-  apply auto[1]
   apply (simp add: fresh_star_def fresh_def)
+  apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
+  apply (simp add: )
   apply (subgoal_tac "x \<in> supp(p \<bullet> t)")
-  apply (smt IntI inf_le1 inter_eqvt subsetD supp_eqvt)
+  apply (metis inf1I inter_eqvt mem_def supp_eqvt )
   apply (rotate_tac 6)
   apply (drule sym)
   apply (simp add: subst_eqvt)
@@ -446,7 +448,7 @@
   apply (simp add: fresh_star_def fresh_def)
   apply blast
   done
-*)
+
 
 text {* Some Tests about Alpha-Equality *}