src/HOL/Tools/Function/induction_schema.ML

     val induct_rule =
       @{thm "wf_induct_rule"}
       |> (curry op COMP) wf_thm
       |> (curry op COMP) istep
 
-    val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
+    val steps_sorted = map snd (sort (int_ord o apply2 fst) steps)
   in
     (steps_sorted, induct_rule)
   end
 
 

     val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
     val R = Free (Rn, mk_relT ST)
     val x = Free (xn, ST)
     val cert = cterm_of (Proof_Context.theory_of ctxt)
 
-    val ineqss = mk_ineqs R scheme
-      |> map (map (pairself (Thm.assume o cert)))
+    val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert)))
     val complete =
       map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
     val wf_thm = mk_wf R scheme |> cert |> Thm.assume
 
     val (descent, pres) = split_list (flat ineqss)