equal
deleted
inserted
replaced
24 val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms |
24 val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms |
25 in |
25 in |
26 fold_map Quotient_Type.add_quotient_type qty_args2 lthy |
26 fold_map Quotient_Type.add_quotient_type qty_args2 lthy |
27 end |
27 end |
28 |
28 |
|
29 |
29 (* defines quotient constants *) |
30 (* defines quotient constants *) |
30 fun qconst_defs qtys const_spec lthy = |
31 fun qconst_defs qtys consts_specs lthy = |
31 let |
32 let |
32 val (qconst_infos, lthy') = fold_map (Quotient_Def.lift_raw_const qtys) const_spec lthy |
33 val (qconst_infos, lthy') = |
|
34 fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy |
33 val phi = ProofContext.export_morphism lthy' lthy |
35 val phi = ProofContext.export_morphism lthy' lthy |
34 in |
36 in |
35 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
37 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
36 end |
38 end |
37 |
39 |