diff -r 65a546c2b8ed -r 7ef6ba42914b LList.thy
--- 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