equal
deleted
inserted
replaced
904 ||>> mk_Freess' "z" setFTss |
904 ||>> mk_Freess' "z" setFTss |
905 ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT |
905 ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT |
906 ||>> mk_Frees "f" fTs |
906 ||>> mk_Frees "f" fTs |
907 ||>> mk_Frees "s" rec_sTs; |
907 ||>> mk_Frees "s" rec_sTs; |
908 |
908 |
909 val Izs = map2 retype_free Ts zs; |
909 val Izs = map2 retype_const_or_free Ts zs; |
910 val phis = map2 retype_free (map mk_pred1T Ts) init_phis; |
910 val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis; |
911 val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis; |
911 val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis; |
912 |
912 |
913 fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_"); |
913 fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_"); |
914 val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind; |
914 val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind; |
915 |
915 |
916 fun ctor_spec abs str map_FT_init = |
916 fun ctor_spec abs str map_FT_init = |