720 ML {*

   721 fun build_alpha_alphabn fv_alphas_lst inducts eq_iff ctxt  =

   722 let

   723   val (fvs_alphas, ls) = split_list fv_alphas_lst;

   724   val (_, alpha_ts) = split_list fvs_alphas;

   725   val tys = map (domain_type o fastype_of) alpha_ts;

   726   val names = Datatype_Prop.make_tnames tys;

   727   val names2 = Name.variant_list names names;

   728   val args = map Free (names ~~ tys);

   729   val args2 = map Free (names2 ~~ tys);

   730   fun alpha_alphabn ((alpha, (arg, arg2)), (no, l)) =

   731     if l = [] then [] else

   732     let

   733       val alpha_bns = map snd l;

   734       val lhs = alpha $ arg $ arg2;

   735       val rhs = foldr1 HOLogic.mk_conj (map (fn x => x $ arg $ arg2) alpha_bns);

   736       val gl = Logic.mk_implies (HOLogic.mk_Trueprop lhs, HOLogic.mk_Trueprop rhs);

   737       fun tac _ = (etac (nth inducts no) THEN_ALL_NEW TRY o rtac @{thm TrueI}

   738         THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps eq_iff)) 1

   739       val th = Goal.prove ctxt (names @ names2) [] gl tac;

   740     in

   741       Project_Rule.projects ctxt (1 upto length l) th

   742     end;

   743   val eqs = map alpha_alphabn ((alpha_ts ~~ (args ~~ args2)) ~~ ((0 upto (length ls - 1)) ~~ ls));

   744 in

   745   flat eqs

   746 end

   747 *}

   748 

   749