--- a/src/Provers/simp.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/Provers/simp.ML Thu Nov 28 10:44:24 1996 +0100
@@ -565,7 +565,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);
- in map eta_Var (ixs ~~ (take(n+1,Ts))) end
+ in ListPair.map eta_Var (ixs, 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)
in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;