equal
deleted
inserted
replaced
69 ML {* |
69 ML {* |
70 fun define_fv_alpha_export dt binds bns ctxt = |
70 fun define_fv_alpha_export dt binds bns ctxt = |
71 let |
71 let |
72 val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') = |
72 val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') = |
73 define_fv dt binds bns ctxt; |
73 define_fv dt binds bns ctxt; |
74 val fv_ts_nobn = take (length bns) fv_ts_loc |
|
75 val (alpha, ctxt'') = |
74 val (alpha, ctxt'') = |
76 define_alpha dt binds bns fv_ts_nobn ctxt'; |
75 define_alpha dt binds bns fv_ts_loc ctxt'; |
77 val alpha_ts_loc = #preds alpha |
76 val alpha_ts_loc = #preds alpha |
78 val alpha_induct_loc = #induct alpha |
77 val alpha_induct_loc = #induct alpha |
79 val alpha_intros_loc = #intrs alpha; |
78 val alpha_intros_loc = #intrs alpha; |
80 val alpha_cases_loc = #elims alpha |
79 val alpha_cases_loc = #elims alpha |
81 val morphism = ProofContext.export_morphism ctxt'' ctxt; |
80 val morphism = ProofContext.export_morphism ctxt'' ctxt; |