src/Pure/proofterm.ML

       | (Const (a, T), Const (b, U))  =>
           if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch
       | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
       | (Bound i, Bound j) => if i=j then instsp else raise PMatch
       | _ => raise PMatch
-  in mtch instsp (pairself Envir.beta_eta_contract p) end;
+  in mtch instsp (apply2 Envir.beta_eta_contract p) end;
 
 fun match_proof Ts tymatch =
   let
     fun optmatch _ inst (NONE, _) = inst
       | optmatch _ _ (SOME _, NONE) = raise PMatch