case is defined using pattern-matching

--- a/src/ZF/Sum.thy	Thu May 04 02:01:24 1995 +0200
+++ b/src/ZF/Sum.thy	Thu May 04 02:01:49 1995 +0200
@@ -18,7 +18,7 @@
     sum_def     "A+B == {0}*A Un {1}*B"
     Inl_def     "Inl(a) == <0,a>"
     Inr_def     "Inr(b) == <1,b>"
-    case_def    "case(c,d) == split(%y z. cond(y, d(z), c(z)))"
+    case_def    "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"
 
   (*operator for selecting out the various summands*)
     Part_def	"Part(A,h) == {x: A. EX z. x = h(z)}"