
diff -r 0440bc1a2438 -r 14c7d7e29c44 Tutorial/Tutorial2.thy
--- 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




