653 end

   653 

   654 ML {*

   655 fun define_fv_alpha_export dt binds bns ctxt =

   656 let

   657   val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') =

   658     define_fv dt binds bns ctxt;

   659   val (alpha, ctxt'') =

   660     define_alpha dt binds bns fv_ts_loc ctxt';

   661   val alpha_ts_loc = #preds alpha

   662   val alpha_induct_loc = #induct alpha

   663   val alpha_intros_loc = #intrs alpha;

   664   val alpha_cases_loc = #elims alpha

   665   val morphism = ProofContext.export_morphism ctxt'' ctxt;

   666   val fv_ts = map (Morphism.term morphism) fv_ts_loc;

   667   val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc;

   668   val fv_def = Morphism.fact morphism fv_def_loc;

   669   val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;

   670   val alpha_induct = Morphism.thm morphism alpha_induct_loc;

   671   val alpha_intros = Morphism.fact morphism alpha_intros_loc

   672   val alpha_cases = Morphism.fact morphism alpha_cases_loc

   673 in

   674   ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'')

   675 end;

   676 *}

   677 

   678 end