src/HOL/Tools/coinduction.ML

           val names_ctxt = ctxt
             |> fold Variable.declare_names vars
             |> fold Variable.declare_thm (raw_thm :: prems);
           val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
           val (rhoTs, rhots) = Thm.match (thm_concl, concl)
-            |>> map (pairself typ_of)
-            ||> map (pairself term_of);
+            |>> map (apply2 typ_of)
+            ||> map (apply2 term_of);
           val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
             |> map (subst_atomic_types rhoTs);
           val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
           val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
             |>> (fn names => Variable.variant_fixes names names_ctxt) ;