tuned proof;

--- a/src/FOL/ex/Classical.thy	Fri May 13 14:26:51 2011 +0200
+++ b/src/FOL/ex/Classical.thy	Fri May 13 14:39:55 2011 +0200
@@ -436,7 +436,7 @@
                   ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b)))))  
    -->                   
    ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
-by (tactic{*Blast.depth_tac @{claset} 12 1*})
+by (blast 12)
    --{*Needed because the search for depths below 12 is very slow*}