src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

               map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings;
 
           val all_proto_sels = flat (@{map 3} (fn k => fn xs => map (pair k o pair xs)) ks xss xss);
           val sel_infos =
             AList.group (op =) (sel_binding_index ~~ all_proto_sels)
-            |> sort (int_ord o pairself fst)
+            |> sort (int_ord o apply2 fst)
             |> map snd |> curry (op ~~) uniq_sel_bindings;
           val sel_bindings = map fst sel_infos;
 
           val sel_defaults =
             if null sel_default_eqs then

 
     fun after_qed ([exhaust_thm] :: thmss) lthy =
       let
         val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
 
-        val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
+        val rho_As = map (apply2 (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
 
         fun inst_thm t thm =
           Drule.instantiate' [] [SOME (certify lthy t)]
             (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
 

                  mk_Trueprop_eq (eta_ufcase, eta_vgcase));
             val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
           in
             (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
              Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
-            |> pairself (singleton (Proof_Context.export names_lthy lthy) #>
+            |> apply2 (singleton (Proof_Context.export names_lthy lthy) #>
               Thm.close_derivation)
           end;
 
         val split_lhs = q $ ufcase;