diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -13,7 +13,7 @@
 structure RewriteHOLProof : REWRITE_HOL_PROOF =
 struct
 
-val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
+val rews = map (apply2 (Proof_Syntax.proof_of_term @{theory} true) o
     Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
 
   (** eliminate meta-equality rules **)