--- a/LList.thy Mon Jan 24 16:03:03 1994 +0100
+++ b/LList.thy Wed Jan 26 17:53:27 1994 +0100
@@ -75,7 +75,7 @@
LList_corec_fun_def
"LList_corec_fun(k,f) == \
\ nat_rec(k, %x. {}, \
-\ %j r x. case(f(x), %u.NIL, \
+\ %j r x. sum_case(f(x), %u.NIL, \
\ %v. split(v, %z w. CONS(z, r(w)))))"
LList_corec_def
@@ -83,7 +83,7 @@
llist_corec_def
"llist_corec(a,f) == \
-\ Abs_LList(LList_corec(a, %z.case(f(z), %x.Inl(x), \
+\ Abs_LList(LList_corec(a, %z.sum_case(f(z), %x.Inl(x), \
\ %y.split(y, %v w. Inr(<Leaf(v), w>)))))"
llistD_Fun_def