# HG changeset patch
# User blanchet
# Date 1346836286 -7200
# Node ID 881e573a619e22bec77da1cb551fb9df03d8bfe4
# Parent  166f19b4677b572b0b69cc7c18753ddef035b77b
added TODO

diff -r 166f19b4677b -r 881e573a619e src/HOL/Codatatype/Tools/bnf_wrap.ML
--- 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;