# HG changeset patch
# User wenzelm
# Date 1305290395 -7200
# Node ID 3a84b69479325fcb3983fb0cc7a964df6d5efbe1
# Parent  9984232a0c68368d62678669555756886606e24d
tuned proof;

diff -r 9984232a0c68 -r 3a84b6947932 src/FOL/ex/Classical.thy
--- 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*}