--- a/Tutorial/Tutorial2.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Tutorial/Tutorial2.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -376,7 +376,7 @@
   moreover 
   have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto
   ultimately 
-  have "atom x \<sharp> Var x" using unbind_fake by auto
+  have "atom x \<sharp> Var x" using unbind_fake by blast
   then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base)
   then show "False" by simp
 qed