--- a/src/HOL/Lambda/Confluence.thy	Thu Jun 22 17:13:05 1995 +0200
+++ b/src/HOL/Lambda/Confluence.thy	Fri Jun 23 09:15:09 1995 +0200
@@ -14,7 +14,7 @@
 
 defs
   diamond_def
-  "diamond(R) == !x y z. (x,y):R --> (x,z):R --> (EX u. (y,u):R & (z,u):R)" 
+  "diamond(R) == !x y.(x,y):R --> (!z.(x,z):R --> (EX u. (y,u):R & (z,u):R))" 
 
   confluent_def "confluent(R) == diamond(R^*)"