--- a/src/HOLCF/Cprod3.thy Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Cprod3.thy Fri Nov 29 12:22:22 1996 +0100
@@ -82,6 +82,9 @@
(* reverse translation <= does not work yet !! *)
(* start 8bit 1 *)
+translations
+ "Let x = a in e" == "CLet`a`(¤ x.e)"
+
(* end 8bit 1 *)
end