src/HOL/Codatatype/Tools/bnf_wrap.ML
changeset 49150 881e573a619e
parent 49148 93f281430e77
child 49152 feb984727eec
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:08:18 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:11:26 2012 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4  
     1.5  fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
     1.6  
     1.7 +(* TODO: provide a way to have a different default value, e.g. "tl Nil = Nil" *)
     1.8  fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
     1.9  
    1.10  fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;