496 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
496 map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs |
497 |
497 |
498 val qsize_descr = |
498 val qsize_descr = |
499 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
499 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
500 |
500 |
501 val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = |
501 val qperm_bn_descr = |
|
502 map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns |
|
503 |
|
504 |
|
505 val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qpermute_bns), lthy8) = |
502 if get_STEPS lthy > 24 |
506 if get_STEPS lthy > 24 |
503 then |
507 then |
504 lthy7 |
508 lthy7 |
505 |> define_qconsts qtys qconstrs_descr |
509 |> define_qconsts qtys qconstrs_descr |
506 ||>> define_qconsts qtys qbns_descr |
510 ||>> define_qconsts qtys qbns_descr |
507 ||>> define_qconsts qtys qfvs_descr |
511 ||>> define_qconsts qtys qfvs_descr |
508 ||>> define_qconsts qtys qfv_bns_descr |
512 ||>> define_qconsts qtys qfv_bns_descr |
509 ||>> define_qconsts qtys qalpha_bns_descr |
513 ||>> define_qconsts qtys qalpha_bns_descr |
|
514 ||>> define_qconsts qtys qperm_bn_descr |
510 else raise TEST lthy7 |
515 else raise TEST lthy7 |
511 |
516 |
512 (* definition of the quotient permfunctions and pt-class *) |
517 (* definition of the quotient permfunctions and pt-class *) |
513 val lthy9 = |
518 val lthy9 = |
514 if get_STEPS lthy > 25 |
519 if get_STEPS lthy > 25 |