321 val qty_full_names = map (fst o dest_Type) qtys |
321 val qty_full_names = map (fst o dest_Type) qtys |
322 val qty_names = map Long_Name.base_name qty_full_names |
322 val qty_names = map Long_Name.base_name qty_full_names |
323 |
323 |
324 val _ = trace_msg (K "Defining the quotient constants...") |
324 val _ = trace_msg (K "Defining the quotient constants...") |
325 val qconstrs_descrs = |
325 val qconstrs_descrs = |
326 (map2 o map2) (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) (get_cnstrs dts) raw_constrs |
326 (map2 o map2) (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) (get_cnstrs dts) raw_constrs |
327 |
327 |
328 val qbns_descr = |
328 val qbns_descr = |
329 map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns |
329 map2 (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) bn_funs raw_bns |
330 |
330 |
331 val qfvs_descr = |
331 val qfvs_descr = |
332 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs |
332 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs |
333 |
333 |
334 val qfv_bns_descr = |
334 val qfv_bns_descr = |
335 map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns |
335 map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.name b, t, NoSyn)) bn_funs raw_fv_bns |
336 |
336 |
337 val qalpha_bns_descr = |
337 val qalpha_bns_descr = |
338 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms |
338 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.name b, t, NoSyn)) bn_funs alpha_bn_trms |
339 |
339 |
340 val qperm_descr = |
340 val qperm_descr = |
341 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
341 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
342 |
342 |
343 val qsize_descr = |
343 val qsize_descr = |
344 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
344 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
345 |
345 |
346 val qperm_bn_descr = |
346 val qperm_bn_descr = |
347 map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns |
347 map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.name b, t, NoSyn)) bn_funs raw_perm_bns |
348 |
348 |
349 val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), |
349 val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), |
350 lthy8) = |
350 lthy8) = |
351 lthy7 |
351 lthy7 |
352 |> fold_map (define_qconsts qtys) qconstrs_descrs |
352 |> fold_map (define_qconsts qtys) qconstrs_descrs |