213 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
213 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
214 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
214 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
215 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
215 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
216 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
216 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
217 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
217 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
|
218 val alpha_bnnames = map (fn (bn, _, _) => "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bns; |
|
219 val alpha_bntypes = map (fn (_, i, _) => @{typ perm} --> nth_dtyp i --> nth_dtyp i --> @{typ bool}) bns; |
|
220 val alpha_bnfrees = map Free (alpha_bnnames ~~ alpha_bntypes); |
218 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
221 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
219 let |
222 let |
220 val Ts = map (typ_of_dtyp descr sorts) dts; |
223 val Ts = map (typ_of_dtyp descr sorts) dts; |
221 val bindslen = length bindcs |
224 val bindslen = length bindcs |
222 val pi_strs_same = replicate bindslen "pi" |
225 val pi_strs_same = replicate bindslen "pi" |