563 |
563 |
564 |
564 |
565 fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = |
565 fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = |
566 let fun xn_list(x,n) = |
566 let fun xn_list(x,n) = |
567 let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n); |
567 let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n); |
568 in map eta_Var (ixs ~~ (take(n+1,Ts))) end |
568 in ListPair.map eta_Var (ixs, take(n+1,Ts)) end |
569 val lhs = list_comb(f,xn_list("X",k-1)) |
569 val lhs = list_comb(f,xn_list("X",k-1)) |
570 val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) |
570 val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) |
571 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
571 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
572 |
572 |
573 fun find_subst tsig T = |
573 fun find_subst tsig T = |