changeset 33063 | 4d462963a7db |
parent 33040 | cffdb7b28498 |
child 33245 | 65232054ffd0 |
--- a/src/FOLP/simp.ML Thu Oct 22 10:52:07 2009 +0200 +++ b/src/FOLP/simp.ML Thu Oct 22 13:48:06 2009 +0200 @@ -534,7 +534,7 @@ fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = let fun xn_list(x,n) = - let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n); + let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1); in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end val lhs = list_comb(f,xn_list("X",k-1)) val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)