--- a/Sum.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/Sum.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -40,8 +40,8 @@
 defs
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
-  sum_case_def  "sum_case(f, g, p) == @z.  (!x. p=Inl(x) --> z=f(x))      \
-\                                        & (!y. p=Inr(y) --> z=g(y))"
+  sum_case_def  "sum_case(f, g, p) == @z.  (!x. p=Inl(x) --> z=f(x))      
+                                        & (!y. p=Inr(y) --> z=g(y))"
 
   sum_def       "A plus B == (Inl``A) Un (Inr``B)"