diff -r 7cbff1da8578 -r 8dbf9ca61ce5 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Thu May 02 10:20:15 1996 +0200
+++ b/src/HOL/ex/cla.ML	Thu May 02 12:00:37 1996 +0200
@@ -314,8 +314,10 @@
     "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) -->            \
 \          (? z. ? w. p(z) & r x w & r w z))  =                 \
 \    (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) &  \
-\          (~p(a) | ~(? y. p(y) & r x y) |                              \
+\          (~p(a) | ~(? y. p(y) & r x y) |                      \
 \           (? z. ? w. p(z) & r x w & r w z)))";
+by (deepen_tac HOL_cs 0 1);  (*beats fast_tac!*)
+result();
 
 writeln"Problem 39";
 goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))";