src/Pure/Tools/rule_insts.ML

     (* result *)
 
     val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
     val inst_vars = map_filter (make_inst inst2) vars2;
   in
-    (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
+    (map (apply2 certT) inst_tvars, map (apply2 cert) inst_vars)
   end;
 
 fun where_rule ctxt mixed_insts fixes thm =
   let
     val ctxt' = ctxt

         val envT' = map (fn (ixn, T) =>
           (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
         val cenv =
           map
             (fn (xi, t) =>
-              pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
+              apply2 (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
             (distinct
               (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
               (xis ~~ ts));
         (* Lift and instantiate rule *)
         val maxidx = Thm.maxidx_of st;

               Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
           | liftvar t = raise TERM("Variable expected", [t]);
         fun liftterm t =
           fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
         fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
-        val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
+        val lifttvar = apply2 (ctyp_of thy o Logic.incr_tvar inc);
         val rule = Drule.instantiate_normalize
               (map lifttvar envT', map liftpair cenv)
               (Thm.lift_rule cgoal thm)
       in
         compose_tac ctxt' (bires_flag, rule, nprems_of thm) i