--- a/src/HOLCF/One.thy Fri Oct 06 16:17:08 1995 +0100
+++ b/src/HOLCF/One.thy Fri Oct 06 17:25:24 1995 +0100
@@ -35,6 +35,10 @@
defs
one_def "one == abs_one`(up`UU)"
one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
+
+translations
+ "case l of one => t1" == "one_when`t1`l"
+
end