diff -r 3f4976d8c97f -r f353b187526a ex/cla.ML
--- a/ex/cla.ML	Thu Jul 21 10:52:00 1994 +0200
+++ b/ex/cla.ML	Wed Jul 27 19:08:40 1994 +0200
@@ -163,6 +163,10 @@
 by (best_tac HOL_dup_cs 1);
 result();
 
+goal HOL.thy "? x. (? y. P(y)) --> P(x)";
+by (best_tac HOL_dup_cs 1);
+result();
+
 writeln"Hard examples with quantifiers";
 
 writeln"Problem 18";