src/Pure/drule.ML

         val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0);
         val certT = ctyp_of thy;
         val instT =
           Vartab.fold (fn (xi, (S, T)) =>
             cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye [];
-        val inst = map (pairself (Thm.instantiate_cterm (instT, []))) ctpairs;
+        val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs;
       in instantiate_normalize (instT, inst) th end
       handle TERM (msg, _) => raise THM (msg, 0, [th])
         | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
 end;