diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/ex/foundn.ML
--- a/src/FOL/ex/foundn.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/foundn.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -99,7 +99,7 @@
 
 
 (*Parallel lifting example. *)
-goal IFOL.thy "EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";
+goal IFOL.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
 by (resolve_tac [exI, allI] 1);
 by (resolve_tac [exI, allI] 1);
 by (resolve_tac [exI, allI] 1);
@@ -108,7 +108,7 @@
 
 
 val prems =
-goal IFOL.thy "(EX z.F(z)) & B ==> (EX z. F(z) & B)";
+goal IFOL.thy "(EX z. F(z)) & B ==> (EX z. F(z) & B)";
 by (rtac conjE 1);
 by (resolve_tac prems 1);
 by (rtac exE 1);