59 *} |
59 *} |
60 |
60 |
61 ML {* |
61 ML {* |
62 fun define_fv_alpha_export dt binds bns ctxt = |
62 fun define_fv_alpha_export dt binds bns ctxt = |
63 let |
63 let |
64 val (((fv_ts_loc, fv_def_loc), alpha), ctxt') = |
64 val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') = |
65 define_fv_alpha dt binds bns ctxt; |
65 define_fv_alpha dt binds bns ctxt; |
66 val alpha_ts_loc = #preds alpha |
66 val alpha_ts_loc = #preds alpha |
67 val alpha_induct_loc = #induct alpha |
67 val alpha_induct_loc = #induct alpha |
68 val alpha_intros_loc = #intrs alpha; |
68 val alpha_intros_loc = #intrs alpha; |
69 val alpha_cases_loc = #elims alpha |
69 val alpha_cases_loc = #elims alpha |
70 val morphism = ProofContext.export_morphism ctxt' ctxt; |
70 val morphism = ProofContext.export_morphism ctxt' ctxt; |
71 val fv_ts = map (Morphism.term morphism) fv_ts_loc; |
71 val fv_ts = map (Morphism.term morphism) fv_ts_loc; |
|
72 val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc; |
72 val fv_def = Morphism.fact morphism fv_def_loc; |
73 val fv_def = Morphism.fact morphism fv_def_loc; |
73 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; |
74 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; |
74 val alpha_induct = Morphism.thm morphism alpha_induct_loc; |
75 val alpha_induct = Morphism.thm morphism alpha_induct_loc; |
75 val alpha_intros = Morphism.fact morphism alpha_intros_loc |
76 val alpha_intros = Morphism.fact morphism alpha_intros_loc |
76 val alpha_cases = Morphism.fact morphism alpha_cases_loc |
77 val alpha_cases = Morphism.fact morphism alpha_cases_loc |
77 in |
78 in |
78 (((fv_ts, fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt') |
79 ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt') |
79 end; |
80 end; |
80 *} |
81 *} |
81 |
82 |
82 end |
83 end |
83 |
84 |