--- a/src/Pure/Isar/proof_context.ML Wed Nov 26 16:55:43 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Nov 26 20:05:34 2014 +0100
@@ -1176,7 +1176,7 @@
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
@@ -1255,7 +1255,7 @@
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)) =