equal
deleted
inserted
replaced
62 rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys 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 qtys spec ctxt = |
|
68 let |
|
69 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |
|
70 val (ts_loc, defs_loc) = split_list result; |
|
71 val morphism = ProofContext.export_morphism ctxt' ctxt; |
|
72 val ts = map (Morphism.term morphism) ts_loc |
|
73 val defs = Morphism.fact morphism defs_loc |
|
74 in |
|
75 (ts, defs, ctxt') |
|
76 end |
|
77 *} |
|
78 |
|
79 ML {* |
|
80 fun define_fv_alpha_export dt binds bns ctxt = |
67 fun define_fv_alpha_export dt binds bns ctxt = |
81 let |
68 let |
82 val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') = |
69 val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') = |
83 define_fv_alpha dt binds bns ctxt; |
70 define_fv_alpha dt binds bns ctxt; |
84 val alpha_ts_loc = #preds alpha |
71 val alpha_ts_loc = #preds alpha |