src/HOL/Nominal/nominal_inductive.ML

              | SOME cargs => fst (fold (fn (xs, x) => fn (bs', cargs') =>
                  let val (cargs1, (u, _) :: cargs2) = chop (length xs) cargs'
                  in (add_binders thy i u
                    (fold (fn (u, T) =>
                       if exists (fn j => j < i) (loose_bnos u) then I
-                      else insert (op aconv o pairself fst)
+                      else insert (op aconv o apply2 fst)
                         (incr_boundvars (~i) u, T)) cargs1 bs'), cargs2)
                  end) cargs (bs, ts ~~ Ts))))
       | _ => fold (add_binders thy i) ts bs)
     | (u, ts) => add_binders thy i u (fold (add_binders thy i) ts bs))
   | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs

     val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
     val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
       HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
     val ps = map (fst o snd) concls;
 
-    val _ = (case duplicates (op = o pairself fst) avoids of
+    val _ = (case duplicates (op = o apply2 fst) avoids of
         [] => ()
       | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
     val _ = avoids |> forall (fn (a, xs) => null (duplicates (op =) xs) orelse
       error ("Duplicate variable names for case " ^ quote a));
     val _ = (case subtract (op =) induct_cases (map fst avoids) of

                      else pi2
                    end;
                  val pis'' = fold (concat_perm #> map) pis' pis;
                  val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
                    (Vartab.empty, Vartab.empty);
-                 val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
+                 val ihyp' = Thm.instantiate ([], map (apply2 (cterm_of thy))
                    (map (Envir.subst_term env) vs ~~
                     map (fold_rev (NominalDatatype.mk_perm [])
                       (rev pis' @ pis)) params' @ [z])) ihyp;
                  fun mk_pi th =
                    Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]