diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/LList.thy
--- a/src/HOL/ex/LList.thy	Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/ex/LList.thy	Fri Mar 24 12:30:35 1995 +0100
@@ -19,8 +19,8 @@
 Previous definition of llistD_Fun was explicit:
   llistD_Fun_def
    "llistD_Fun(r) == 	\
-\       {<LNil,LNil>}  Un  	\
-\       (UN x. (split(%l1 l2.<LCons(x,l1),LCons(x,l2)>))``r)"
+\       {(LNil,LNil)}  Un  	\
+\       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
 *)
 
 LList = Gfp + SList +
@@ -69,9 +69,9 @@
 
 coinductive "LListD(r)"
   intrs
-    NIL_I  "<NIL, NIL> : LListD(r)"
-    CONS_I "[| <a,b>: r;  <M,N> : LListD(r)   \
-\	    |] ==> <CONS a M, CONS b N> : LListD(r)"
+    NIL_I  "(NIL, NIL) : LListD(r)"
+    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   \
+\	    |] ==> (CONS a M, CONS b N) : LListD(r)"
 
 defs
   (*Now used exclusively for abbreviating the coinduction rule*)
@@ -79,9 +79,9 @@
 \		  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
 
   LListD_Fun_def "LListD_Fun r X ==   \
-\		  {z. z = <NIL, NIL> |   \
-\		      (? M N a b. z = <CONS a M, CONS b N> &   \
-\		                  <a, b> : r & <M, N> : X)}"
+\		  {z. z = (NIL, NIL) |   \
+\		      (? M N a b. z = (CONS a M, CONS b N) &   \
+\		                  (a, b) : r & (M, N) : X)}"
 
   (*defining the abstract constructors*)
   LNil_def  	"LNil == Abs_llist(NIL)"
@@ -102,7 +102,7 @@
   llist_corec_def
    "llist_corec a f == \
 \       Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) \
-\                                    (split(%v w. Inr(<Leaf(v), w>))) (f z)))"
+\                                    (split(%v w. Inr((Leaf(v), w)))) (f z)))"
 
   llistD_Fun_def
    "llistD_Fun(r) == 	\
@@ -113,28 +113,28 @@
   Lconst_def	"Lconst(M) == lfp(%N. CONS M N)"     
 
   Lmap_def
-   "Lmap f M == LList_corec M (List_case (Inl Unity) (%x M'. Inr(<f(x), M'>)))"
+   "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
 
   lmap_def
-   "lmap f l == llist_corec l (llist_case (Inl Unity) (%y z. Inr(<f(y), z>)))"
+   "lmap f l == llist_corec l (llist_case (Inl ()) (%y z. Inr((f(y), z))))"
 
-  iterates_def	"iterates f a == llist_corec a (%x. Inr(<x, f(x)>))"     
+  iterates_def	"iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
 
 (*Append generates its result by applying f, where
-    f(<NIL,NIL>) = Inl(Unity)
-    f(<NIL, CONS N1 N2>) = Inr(<N1, <NIL,N2>)
-    f(<CONS M1 M2, N>)    = Inr(<M1, <M2,N>)
+    f((NIL,NIL)) = Inl(())
+    f((NIL, CONS N1 N2)) = Inr((N1, (NIL,N2))
+    f((CONS M1 M2, N))    = Inr((M1, (M2,N))
 *)
 
   Lappend_def
-   "Lappend M N == LList_corec <M,N>	   				     \
-\     (split(List_case (List_case (Inl Unity) (%N1 N2. Inr(<N1, <NIL,N2>>))) \
-\                      (%M1 M2 N. Inr(<M1, <M2,N>>))))"
+   "Lappend M N == LList_corec (M,N)	   				     \
+\     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) \
+\                      (%M1 M2 N. Inr((M1, (M2,N))))))"
 
   lappend_def
-   "lappend l n == llist_corec <l,n>	   				     \
-\   (split(llist_case (llist_case (Inl Unity) (%n1 n2. Inr(<n1, <LNil,n2>>))) \
-\                     (%l1 l2 n. Inr(<l1, <l2,n>>))))"
+   "lappend l n == llist_corec (l,n)	   				     \
+\   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) \
+\                     (%l1 l2 n. Inr((l1, (l2,n))))))"
 
 rules
     (*faking a type definition...*)