src/Pure/Isar/proof_context.ML

 
 (** cases **)
 
 fun dest_cases ctxt =
   Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) []
-  |> sort (int_ord o pairself #1) |> map #2;
+  |> sort (int_ord o apply2 #1) |> map #2;
 
 local
 
 fun update_case _ _ ("", _) res = res
   | update_case _ _ (name, NONE) (cases, index) =

 
 fun pretty_abbrevs show_globals ctxt =
   let
     val space = const_space ctxt;
     val (constants, global_constants) =
-      pairself (#constants o Consts.dest) (#consts (rep_data ctxt));
+      apply2 (#constants o Consts.dest) (#consts (rep_data ctxt));
     val globals = Symtab.make global_constants;
     fun add_abbr (_, (_, NONE)) = I
       | add_abbr (c, (T, SOME t)) =
           if not show_globals andalso Symtab.defined globals c then I
           else cons (c, Logic.mk_equals (Const (c, T), t));