src/Pure/thm.ML

 
 fun crep_thm (Thm (_, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
   let fun cterm max t = Cterm {thy = thy, t = t, T = propT, maxidx = max, sorts = shyps} in
    {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps,
     hyps = map (cterm ~1) hyps,
-    tpairs = map (pairself (cterm maxidx)) tpairs,
+    tpairs = map (apply2 (cterm maxidx)) tpairs,
     prop = cterm maxidx prop}
   end;
 
 fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
   fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;

   Unify.smash_unifiers (make_context opt_ctxt thy) tpairs (Envir.empty maxidx)
   |> Seq.map (fn env =>
       if Envir.is_empty env then th
       else
         let
-          val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
+          val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
             (*remove trivial tpairs, of the form t==t*)
             |> filter_out (op aconv);
           val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
           val prop' = Envir.norm_term env prop;
           val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');

         val _ = exists bad_term hyps andalso
           raise THM ("generalize: variable free in assumptions", 0, [th]);
 
         val gen = Term_Subst.generalize (tfrees, frees) idx;
         val prop' = gen prop;
-        val tpairs' = map (pairself gen) tpairs;
+        val tpairs' = map (apply2 gen) tpairs;
         val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
       in
         Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
          {thy = thy,
           tags = [],

        {thy = merge_thys1 goal orule,
         tags = [],
         maxidx = maxidx + inc,
         shyps = Sorts.union shyps sorts,  (*sic!*)
         hyps = hyps,
-        tpairs = map (pairself lift_abs) tpairs,
+        tpairs = map (apply2 lift_abs) tpairs,
         prop = Logic.list_implies (map lift_all As, lift_all B)})
   end;
 
 fun incr_indexes i (thm as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) =
   if i < 0 then raise THM ("negative increment", 0, [thm])

      {thy = thy,
       tags = [],
       maxidx = maxidx + i,
       shyps = shyps,
       hyps = hyps,
-      tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs,
+      tpairs = map (apply2 (Logic.incr_indexes ([], i))) tpairs,
       prop = Logic.incr_indexes ([], i) prop});
 
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
 fun assumption opt_ctxt i state =
   let

         maxidx = Envir.maxidx_of env,
         shyps = Envir.insert_sorts env shyps,
         hyps = hyps,
         tpairs =
           if Envir.is_empty env then tpairs
-          else map (pairself (Envir.norm_term env)) tpairs,
+          else map (apply2 (Envir.norm_term env)) tpairs,
         prop =
           if Envir.is_empty env then (*avoid wasted normalizations*)
             Logic.list_implies (Bs, C)
           else (*normalize the new rule fully*)
             Envir.norm_term env (Logic.list_implies (Bs, C)),

           |> fold (add_var o fst) dpairs
           |> fold (add_var o fst) tpairs
           |> fold (add_var o snd) tpairs;
         val vids' = fold (add_var o strip_lifted B) As [];
         (*unknowns appearing elsewhere be preserved!*)
-        val al' = distinct ((op =) o pairself fst)
+        val al' = distinct ((op =) o apply2 fst)
           (filter_out (fn (x, y) =>
              not (member (op =) vids' x) orelse
              member (op =) vids x orelse member (op =) vids y) al);
         val unchanged = filter_out (AList.defined (op =) al') vids';
         fun del_clashing clash xs _ [] qs =

        let val normt = Envir.norm_term env;
            (*perform minimal copying here by examining env*)
            val (ntpairs, normp) =
              if Envir.is_empty env then (tpairs, (Bs @ As, C))
              else
-             let val ntps = map (pairself normt) tpairs
+             let val ntps = map (apply2 normt) tpairs
              in if Envir.above env smax then
                   (*no assignments in state; normalize the rule only*)
                   if lifted
                   then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
                   else (ntps, (Bs @ map normt As, C))