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