--- a/Nominal/TySch.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -36,7 +36,7 @@
   shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))"
   apply(simp add: t_tyS_eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts)
+  apply(simp add: alpha_gen fresh_star_def eqvts)
   apply auto
   done
 
@@ -44,7 +44,7 @@
   shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))"
   apply(simp add: t_tyS_eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff)
 oops
 
 lemma
@@ -53,7 +53,7 @@
   using a
   apply(simp add: t_tyS_eq_iff)
   apply(clarify)
-  apply(simp add: alpha_gen t_tyS_fv fresh_star_def t_tyS_perm eqvts t_tyS_eq_iff)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS_eq_iff)
   apply auto
   done