src/HOL/Tools/datatype_realizer.ML

     val concl =
       HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
         (map (fn ((((i, _), T), U), tname) =>
           make_pred i U T (mk_proj i is r) (Free (tname, T)))
             (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
-    val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
+    val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj
       (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
 
     val thm =
       Goal.prove_internal ctxt (map cert prems) (cert concl)
         (fn prems =>