src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

       | split_arg_mode' m t =
         if eq_mode (m, Input) then (SOME t, NONE)
         else if eq_mode (m, Output) then (NONE,  SOME t)
         else raise Fail "split_map_mode: mode and term do not match"
   in
-    (pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts)
+    (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts)
   end
 
 (* splits mode and maps function to higher-order argument types *)
 fun split_map_modeT f mode Ts =
   let

         end
       | split_arg_mode' Input T = (SOME T, NONE)
       | split_arg_mode' Output T = (NONE,  SOME T)
       | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
   in
-    (pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
+    (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
   end
 
 fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts
 
 fun fold_map_aterms_prodT comb f (Type (@{type_name Product_Type.prod}, [T1, T2])) s =

           end
       | split_arg_mode Input T = ([T], [])
       | split_arg_mode Output T = ([], [T])
       | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match"
   in
-    (pairself flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts)
+    (apply2 flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts)
   end
 
 fun string_of_mode mode =
   let
     fun string_of_mode1 Input = "i"