src/HOL/Codatatype/Tools/bnf_wrap.ML
changeset 49150 881e573a619e
parent 49148 93f281430e77
child 49152 feb984727eec
equal deleted inserted replaced
49149:166f19b4677b 49150:881e573a619e
    49   | mk_half_pairss' indent (y :: ys) =
    49   | mk_half_pairss' indent (y :: ys) =
    50     indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys);
    50     indent @ fold_rev (cons o single o pair y) ys (mk_half_pairss' ([] :: indent) ys);
    51 
    51 
    52 fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
    52 fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
    53 
    53 
       
    54 (* TODO: provide a way to have a different default value, e.g. "tl Nil = Nil" *)
    54 fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
    55 fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
    55 
    56 
    56 fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    57 fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    57 
    58 
    58 fun name_of_ctr t =
    59 fun name_of_ctr t =