src/HOL/TPTP/atp_theory_export.ML

   | ident_of_problem_line (Type_Decl (ident, _, _)) = ident
   | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
   | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
   | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
 
-fun order_facts ord = sort (ord o pairself ident_of_problem_line)
+fun order_facts ord = sort (ord o apply2 ident_of_problem_line)
 
 fun order_problem_facts _ [] = []
   | order_problem_facts ord ((heading, lines) :: problem) =
     if heading = factsN then (heading, order_facts ord lines) :: problem
     else (heading, lines) :: order_problem_facts ord problem

                |> adjust_type_enc format
     val mono = not (is_type_enc_polymorphic type_enc)
     val facts =
       Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
                                   Keyword.empty_keywords [] [] css_table
-      |> sort (Sledgehammer_MaSh.crude_thm_ord o pairself snd)
+      |> sort (Sledgehammer_MaSh.crude_thm_ord o apply2 snd)
     val problem =
       facts
       |> map (fn ((_, loc), th) =>
         ((Thm.get_name_hint th, loc), th |> prop_of |> mono ? monomorphize_term ctxt))
       |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []

         (tl all_problem_names ~~ fst (split_last all_problem_names))
       |> String_Graph.topological_order
     val order_tab =
       Symtab.empty
       |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names))
-    val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
+    val name_ord = int_ord o apply2 (the o Symtab.lookup order_tab)
   in
     problem
     |> (case format of
           DFG _ => I
         | _ => add_inferences_to_problem ctxt format

     val _ = Isabelle_System.mkdir include_dir
     val (prelude, groups) =
       problem_of_theory ctxt thy format infer_policy type_enc
       |> split_last
       ||> (snd
-           #> chop_maximal_groups (op = o pairself theory_name_of_fact)
+           #> chop_maximal_groups (op = o apply2 theory_name_of_fact)
            #> map (`(include_base_name_of_fact o hd)))
     fun write_prelude () =
       let val ss = lines_of_problem ctxt format prelude in
         File.append file_order_path (prelude_base_name ^ "\n");
         write_lines (ap include_dir prelude_name) ss