src/Pure/proofterm.ML

--- a/src/Pure/proofterm.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/Pure/proofterm.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -1226,7 +1226,7 @@
       | (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