src/Pure/context.ML

     val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
     val _ = Synchronized.change kinds (Datatab.update (k, kind));
   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;
 
 
 

   |> insert_id id2;
 
 
 (* 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;
 
 fun subthy thys = eq_thy thys orelse proper_subthy thys;