240      {quiet_mode = true, verbose = false, alt_name = Binding.empty,

   240      {quiet_mode = true, verbose = false, alt_name = Binding.empty,

   241       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}

   241       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}

   242      all_alpha_names [] all_alpha_eqs [] lthy

   242      all_alpha_names [] all_alpha_eqs [] lthy

   243 

   243 

   244   val alpha_ts_loc = #preds alphas;

   244   val alpha_ts_loc = #preds alphas;

   246   val alpha_intros_loc = #intrs alphas;

   246   val alpha_intros_loc = #intrs alphas;

   247   val alpha_cases_loc = #elims alphas;

   247   val alpha_cases_loc = #elims alphas;

   248   val morphism = ProofContext.export_morphism lthy' lthy;

   248   val morphism = ProofContext.export_morphism lthy' lthy;

   249 

   249 

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

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