equal
deleted
inserted
replaced
22 (* permutations for quotient types *) |
22 (* permutations for quotient types *) |
23 |
23 |
24 ML {* |
24 ML {* |
25 fun quotient_lift_consts_export qtys spec ctxt = |
25 fun quotient_lift_consts_export qtys spec ctxt = |
26 let |
26 let |
27 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |
27 val (result, ctxt') = fold_map (Quotient_Def.lift_raw_const qtys) spec ctxt; |
28 val (ts_loc, defs_loc) = split_list result; |
28 val (ts_loc, defs_loc) = split_list (map (fn info => (#qconst info, #def info)) result); |
29 val morphism = ProofContext.export_morphism ctxt' ctxt; |
29 val morphism = ProofContext.export_morphism ctxt' ctxt; |
30 val ts = map (Morphism.term morphism) ts_loc |
30 val ts = map (Morphism.term morphism) ts_loc |
31 val defs = Morphism.fact morphism defs_loc |
31 val defs = Morphism.fact morphism defs_loc |
32 in |
32 in |
33 (ts, defs, ctxt') |
33 (ts, defs, ctxt') |