diff -r 3123fef88dce -r 82aef6857c5b src/Provers/simp.ML
--- 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;