src/FOLP/simp.ML
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)