src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

 fun invalid_map ctxt t =
   error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
 fun unexpected_corec_call ctxt t =
   error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
 
-fun sort_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs);
+fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
 
 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
 val mk_dnf = mk_disjs o map mk_conjs;
 

       nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0;
 
     val coinduct_attrs_pair =
       (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], []));
 
-    val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
+    val perm_fp_sugars = sort (int_ord o apply2 #fp_res_index) fp_sugars;
 
     val indices = map #fp_res_index fp_sugars;
     val perm_indices = map #fp_res_index perm_fp_sugars;
 
     val perm_fpTs = map #T perm_fp_sugars;

           orelse primcorec_error_eqns ("missing equations for function(s): " ^ commas missing) []
       end;
 
     val callssss =
       map_filter (try (fn Sel x => x)) eqns_data
-      |> partition_eq (op = o pairself #fun_name)
+      |> partition_eq (op = o apply2 #fun_name)
       |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
       |> map (flat o snd)
       |> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss
       |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
         (ctr, map (K []) sels))) basic_ctr_specss);

       corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
     val corec_specs = take actual_nn corec_specs';
     val ctr_specss = map #ctr_specs corec_specs;
 
     val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
-      |> partition_eq (op = o pairself #fun_name)
+      |> partition_eq (op = o apply2 #fun_name)
       |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
-      |> map (sort (op < o pairself #ctr_no |> make_ord) o flat o snd);
+      |> map (sort (op < o apply2 #ctr_no |> make_ord) o flat o snd);
 
     val _ = disc_eqnss' |> map (fn x =>
-      let val d = duplicates (op = o pairself #ctr_no) x in null d orelse
-        (if forall (is_some o #ctr_rhs_opt) x then
-          primcorec_error_eqns "multiple equations for constructor(s)"
-            (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d
-              |> map (the o #ctr_rhs_opt)) else
-          primcorec_error_eqns "excess discriminator formula in definition"
-            (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn)) end);
+      let val d = duplicates (op = o apply2 #ctr_no) x in
+        null d orelse
+         (if forall (is_some o #ctr_rhs_opt) x then
+            primcorec_error_eqns "multiple equations for constructor(s)"
+              (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d
+                |> map (the o #ctr_rhs_opt))
+          else
+            primcorec_error_eqns "excess discriminator formula in definition"
+              (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn))
+      end);
 
     val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
-      |> partition_eq (op = o pairself #fun_name)
+      |> partition_eq (op = o apply2 #fun_name)
       |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
       |> map (flat o snd);
 
     val arg_Tss = map (binder_types o snd o fst) fixes;
     val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss

                   NONE => []
                 | SOME (exhaustive_code, rhs, raw_rhs, ctr_thms) =>
                   let
                     val ms = map (Logic.count_prems o prop_of) ctr_thms;
                     val (raw_goal, goal) = (raw_rhs, rhs)
-                      |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
+                      |> apply2 (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
                         #> curry Logic.list_all (map dest_Free fun_args));
                     val (distincts, discIs, _, split_sels, split_sel_asms) =
                       case_thms_of_term lthy raw_rhs;
 
                     val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs split_sels

           |> map sort_list_duplicates;
 
         val ctr_alists = @{map 6} (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists
           (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss;
         val ctr_thmss0 = map (map snd) ctr_alists;
-        val ctr_thmss = map (map (snd o snd) o sort (int_ord o pairself fst)) ctr_alists;
+        val ctr_thmss = map (map (snd o snd) o sort (int_ord o apply2 fst)) ctr_alists;
 
         val code_thmss =
           @{map 6} prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss0 ctr_specss;
 
         val disc_iff_or_disc_thmss =