| changeset 40212 | 20df78048db5 |
| parent 40024 | a0f760ef6995 |
| child 40217 | 656bb85f01ab |
--- a/src/HOLCF/Tools/holcf_library.ML Sun Oct 24 15:11:24 2010 -0700 +++ b/src/HOLCF/Tools/holcf_library.ML Sun Oct 24 15:19:17 2010 -0700 @@ -174,8 +174,8 @@ 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 ***)