diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Ssum3.thy
--- a/src/HOLCF/Ssum3.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Ssum3.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -30,6 +30,9 @@
 "case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s"
 
 (* start 8bit 1 *)
+translations
+"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(¤x.t1)`(¤y.t2)`s"
+
 (* end 8bit 1 *)
 
 end