author | blanchet |
Wed, 05 Sep 2012 11:11:26 +0200 | |
changeset 49150 | 881e573a619e |
parent 49149 | 166f19b4677b |
child 49151 | ff86a2253f05 |
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 05 11:08:18 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 05 11:11:26 2012 +0200 @@ -51,6 +51,7 @@ fun mk_half_pairss ys = mk_half_pairss' [[]] ys; +(* TODO: provide a way to have a different default value, e.g. "tl Nil = Nil" *) fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T); fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;