--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 01 16:13:42 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jun 02 10:09:23 2011 +0900
@@ -427,13 +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)")
-  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)