--- a/Tutorial/Tutorial5.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Tutorial/Tutorial5.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -127,12 +127,13 @@
   obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"
 using ty fc
 apply(cases)
+using [[simproc del: alpha_lst]]
 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
 apply(auto simp add: Abs1_eq_iff)
 apply(rotate_tac 3)
 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
 apply(perm_simp)
-apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)
+apply(auto simp add: flip_fresh_fresh ty_fresh)
 done