# HG changeset patch
# User wenzelm
# Date 849518561 -3600
# Node ID c2f76a5bad65324f1cd2c783a4ee8e8a77686822
# Parent  b239c202c91f3b10d7dc4330b3a5bbd908b2db02
removed out-dated comment;

diff -r b239c202c91f -r c2f76a5bad65 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Mon Dec 02 10:19:52 1996 +0100
+++ b/src/ZF/ZF.thy	Mon Dec 02 10:22:41 1996 +0100
@@ -128,10 +128,9 @@
 
   "<x, y, z>"   == "<x, <y, z>>"
   "<x, y>"      == "Pair(x, y)"
-  "%<x,y,zs>.b"   == "split(%x <y,zs>.b)"
-  "%<x,y>.b"      == "split(%x y.b)"
-(* The <= direction fails if split has more than one argument because
-   ast-matching fails.  Otherwise it would work fine *)
+  "%<x,y,zs>.b" == "split(%x <y,zs>.b)"
+  "%<x,y>.b"    == "split(%x y.b)"
+
 
 defs