--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 01 21:03:30 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 01 22:55:14 2011 +0100
@@ -428,6 +428,8 @@
   apply (simp add: alphas fresh_star_zero)
   apply auto[1]
   apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
+oops
+(*
   apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)
   apply (drule subsetD[OF supp_subst])
   apply auto[1]
@@ -444,7 +446,7 @@
   apply (simp add: fresh_star_def fresh_def)
   apply blast
   done
-
+*)
 
 text {* Some Tests about Alpha-Equality *}