added print translations tha avoid eta contraction for important binders.
(* Title: HOLCF/One.thy ID: $Id$ Author: Oscar Slotosch License: GPL (GNU GENERAL PUBLIC LICENSE)*)One = Lift +types one = unit liftconstdefs ONE :: "one" "ONE == Def ()"translations "one" <= (type) "unit lift" end