--- a/Tutorial/Tutorial2s.thy	Thu Oct 04 12:44:43 2012 +0100
+++ b/Tutorial/Tutorial2s.thy	Fri Oct 19 09:40:24 2012 +0100
@@ -346,7 +346,8 @@
   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" 
+    by (rule_tac unbind_fake) (auto)
   then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base)
   then show "False" by simp
 qed