src/HOLCF/Ssum0.thy

--- a/src/HOLCF/Ssum0.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Ssum0.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -31,7 +31,7 @@
 
   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