diff -r e65b60b28341 -r ca5a7bbbee6c src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Wed Apr 23 11:02:19 1997 +0200
+++ b/src/HOL/ex/cla.ML	Wed Apr 23 11:05:18 1997 +0200
@@ -281,11 +281,10 @@
 writeln"Problem 34  AMENDED (TWICE!!)";
 (*Andrews's challenge*)
 goal HOL.thy "((? x. ! y. p(x) = p(y))  =               \
-\                   ((? x. q(x)) = (! y. p(y))))   =    \
-\                  ((? x. ! y. q(x) = q(y))  =          \
-\                   ((? x. p(x)) = (! y. q(y))))";
+\              ((? x. q(x)) = (! y. p(y))))   =    \
+\             ((? x. ! y. q(x) = q(y))  =          \
+\              ((? x. p(x)) = (! y. q(y))))";
 by (Blast_tac 1);
-(*slower with smaller bounds*)
 result();
 
 writeln"Problem 35";