src/HOLCF/Ssum3.thy

--- a/src/HOLCF/Ssum3.thy	Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Ssum3.thy	Mon Feb 17 10:57:11 1997 +0100
@@ -8,18 +8,13 @@
 
 Ssum3 = Ssum2 +
 
-arities "++" :: (pcpo,pcpo)pcpo                 (* Witness ssum2.ML *)
+instance "++" :: (pcpo,pcpo)pcpo (least_ssum,cpo_ssum)
 
 consts  
         sinl    :: "'a -> ('a++'b)" 
         sinr    :: "'b -> ('a++'b)" 
         sswhen  :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
 
-rules 
-
-inst_ssum_pcpo  "(UU::'a++'b) = Isinl(UU)"
-
-
 defs
 
 sinl_def        "sinl   == (LAM x.Isinl(x))"