src/HOL/Integ/Equiv.ML

--- a/src/HOL/Integ/Equiv.ML	Sun Jul 16 20:55:17 2000 +0200
+++ b/src/HOL/Integ/Equiv.ML	Sun Jul 16 20:55:56 2000 +0200
@@ -209,7 +209,7 @@
 (*Allows a natural expression of binary operators, without explicit calls
   to "split"*)
 Goal "(UN (x1,x2):X. UN (y1,y2):Y. A x1 x2 y1 y2) = \
-\     (UN x:X. UN y:Y. split(%x1 x2. split(%y1 y2. A x1 x2 y1 y2) y) x)";
+\     (UN x:X. UN y:Y. (%(x1, x2). (%(y1, y2). A x1 x2 y1 y2) y) x)";
 by Auto_tac;
 qed "UN_UN_split_split_eq";