src/HOLCF/Tools/holcf_library.ML

 
 (*** Lifted unit type ***)
 
 val oneT = @{typ "one"};
 
-fun one_when_const T = Const (@{const_name one_when}, T ->> oneT ->> T);
-fun mk_one_when t = one_when_const (fastype_of t) ` t;
+fun one_case_const T = Const (@{const_name one_case}, T ->> oneT ->> T);
+fun mk_one_case t = one_case_const (fastype_of t) ` t;
 
 
 (*** Strict product type ***)
 
 fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);