equal
deleted
inserted
replaced
53 Thm.rename_boundvars t (rename_term_bvars t) th |
53 Thm.rename_boundvars t (rename_term_bvars t) th |
54 end; |
54 end; |
55 *} |
55 *} |
56 |
56 |
57 ML {* |
57 ML {* |
58 fun lift_thm ctxt thm = |
58 fun lift_thm qtys ctxt thm = |
59 let |
59 let |
60 val un_raw_names = rename_vars un_raws |
60 val un_raw_names = rename_vars un_raws |
61 in |
61 in |
62 rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))) |
62 rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm)) |
63 end |
63 end |
64 *} |
64 *} |
65 |
65 |
66 ML {* |
66 ML {* |
67 fun quotient_lift_consts_export spec ctxt = |
67 fun quotient_lift_consts_export qtys spec ctxt = |
68 let |
68 let |
69 val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt; |
69 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |
70 val (ts_loc, defs_loc) = split_list result; |
70 val (ts_loc, defs_loc) = split_list result; |
71 val morphism = ProofContext.export_morphism ctxt' ctxt; |
71 val morphism = ProofContext.export_morphism ctxt' ctxt; |
72 val ts = map (Morphism.term morphism) ts_loc |
72 val ts = map (Morphism.term morphism) ts_loc |
73 val defs = Morphism.fact morphism defs_loc |
73 val defs = Morphism.fact morphism defs_loc |
74 in |
74 in |