--- a/Tutorial/Tutorial2.thy	Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial2.thy	Mon Mar 05 16:27:28 2012 +0000
@@ -242,7 +242,7 @@
       by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)
     then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto
   qed
-  ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp
+  ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by (simp only:)
 qed (auto) -- {* var and app cases, luckily, are automatic *}