src/Pure/context.ML

--- a/src/Pure/context.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/Pure/context.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -145,7 +145,7 @@
   in k end;
 
 val extend_data = Datatab.map invoke_extend;
-fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
+fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data;
 
 end;
 
@@ -238,7 +238,7 @@
 
 (* equality and inclusion *)
 
-val eq_thy = op = o pairself (#id o identity_of);
+val eq_thy = op = o apply2 (#id o identity_of);
 
 fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) =
   Inttab.defined ids id;