--- a/src/FOL/FOL_lemmas2.ML Thu Jul 06 13:11:32 2000 +0200
+++ b/src/FOL/FOL_lemmas2.ML Thu Jul 06 13:28:36 2000 +0200
@@ -1,4 +1,4 @@
-Goal "!!a b c. [| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c";
+Goal "[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c";
by (Blast_tac 1);
qed "ex1_functional";