diff -r 94b8b70f7bc0 -r e8cf0520c820 Nominal/ExTySch.thy
--- a/Nominal/ExTySch.thy	Sat Mar 27 08:17:43 2010 +0100
+++ b/Nominal/ExTySch.thy	Sat Mar 27 08:42:07 2010 +0100
@@ -36,7 +36,7 @@
   "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
   apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
   apply (simp_all only: t_raw_tyS_raw.size)
-  apply (simp_all only: alpha_gen)
+  apply (simp_all only: alphas)
   apply clarify
   apply (simp_all only: size_eqvt_raw)
   done
@@ -119,7 +119,7 @@
   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (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)
+  apply(simp add: alphas)
   apply(auto)
   apply(simp add: fresh_star_def fresh_zero_perm)
   done