equal
deleted
inserted
replaced
125 ML {* |
125 ML {* |
126 fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss = |
126 fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss = |
127 let |
127 let |
128 fun mk_alphabn_free (bn, ith, _) = |
128 fun mk_alphabn_free (bn, ith, _) = |
129 let |
129 let |
130 val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
130 val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Free bn))); |
131 val ty = nth_dtyp dt_descr sorts ith; |
131 val ty = nth_dtyp dt_descr sorts ith; |
132 val alphabn_type = ty --> ty --> @{typ bool}; |
132 val alphabn_type = ty --> ty --> @{typ bool}; |
133 val alphabn_free = Free(alphabn_name, alphabn_type); |
133 val alphabn_free = Free(alphabn_name, alphabn_type); |
134 in |
134 in |
135 (alphabn_name, alphabn_free) |
135 (alphabn_name, alphabn_free) |