src/HOLCF/Ssum3.thy

--- a/src/HOLCF/Ssum3.thy	Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Ssum3.thy	Mon Dec 02 12:37:15 1996 +0100
@@ -30,9 +30,6 @@
 "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