--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 09:56:39 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 17:25:54 2011 +0900
@@ -380,7 +380,7 @@
     and S T :: "'b :: fs"
   assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)"
     and f1: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T"
-    and f2: "\<And>x. supp T - atom ` xs \<inter> supp T = supp S - atom ` ys \<inter> supp S \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T"
+    and f2: "\<And>x. supp T - atom ` xs = supp S - atom ` ys \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T"
     and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S
                \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S
  \<Longrightarrow> p \<bullet> (f xs T) = f ys S"
@@ -401,7 +401,9 @@
   apply (subst fresh_star_Un)
   apply (rule conjI)
   apply (simp add: fresh_star_def f1)
+  apply (subgoal_tac "supp T - atom ` xs = supp S - atom ` ys")
   apply (simp add: fresh_star_def f2)
+  apply blast
   apply (simp add: eqv)
   done