src/HOLCF/Ssum0.thy

   Isinl_def     "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
   Isinr_def     "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
 
   Iwhen_def     "Iwhen(f)(g)(s) == @z.
                                     (s=Isinl(UU) --> z=UU)
-                        &(!a. a~=UU & s=Isinl(a) --> z=f`a)  
-                        &(!b. b~=UU & s=Isinr(b) --> z=g`b)"  
+                        &(!a. a~=UU & s=Isinl(a) --> z=f$a)  
+                        &(!b. b~=UU & s=Isinr(b) --> z=g$b)"  
 
 end