diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -375,7 +375,7 @@
                th ctxt ctxt
     val (cnf_ths, ctxt) = clausify nnf_th
     fun intr_imp ct th =
-      Thm.instantiate ([], map (pairself (cterm_of thy))
+      Thm.instantiate ([], map (apply2 (cterm_of thy))
                                [(Var (("i", 0), @{typ nat}),
                                  HOLogic.mk_nat ax_no)])
                       (zero_var_indexes @{thm skolem_COMBK_D})