equal
deleted
inserted
replaced
365 |
365 |
366 fun mk_disc k = |
366 fun mk_disc k = |
367 ctrXs_Tss |
367 ctrXs_Tss |
368 |> map_index (fn (i, Ts) => |
368 |> map_index (fn (i, Ts) => |
369 Abs (Name.uu, mk_tupleT_balanced Ts, |
369 Abs (Name.uu, mk_tupleT_balanced Ts, |
370 if i + 1 = k then \<^const>\<open>HOL.True\<close> else \<^const>\<open>HOL.False\<close>)) |
370 if i + 1 = k then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>)) |
371 |> mk_case_sumN_balanced |
371 |> mk_case_sumN_balanced |
372 |> map_types substXYT |
372 |> map_types substXYT |
373 |> (fn tm => Library.foldl1 HOLogic.mk_comp [tm, rep, snd_const YpreT]) |
373 |> (fn tm => Library.foldl1 HOLogic.mk_comp [tm, rep, snd_const YpreT]) |
374 |> map_types substAT; |
374 |> map_types substAT; |
375 |
375 |