
diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Ssum3.thy
--- a/src/HOLCF/Ssum3.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Ssum3.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -22,6 +22,6 @@
 sscase_def      "sscase   == (LAM f g s. Iwhen(f)(g)(s))"
 
 translations
-"case s of sinl`x => t1 | sinr`y => t2" == "sscase`(LAM x. t1)`(LAM y. t2)`s"
+"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
 
 end




