src/Pure/ML/ml_env.ML
changeset 59058 a78612c67ec0
parent 56618 874bdedb2313
child 59127 723b11f8ffbf
--- a/src/Pure/ML/ml_env.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/Pure/ML/ml_env.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -57,8 +57,8 @@
   fun extend (data : T) = make_data (false, #tables data, #sml_tables data);
   fun merge (data : T * T) =
     make_data (false,
-      merge_tables (pairself #tables data),
-      merge_tables (pairself #sml_tables data));
+      merge_tables (apply2 #tables data),
+      merge_tables (apply2 #sml_tables data));
 );
 
 val inherit = Env.put o Env.get;
@@ -85,7 +85,7 @@
         Context.thread_data ()
         |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
         |> append (sel2 ML_Name_Space.global ()))
-      |> sort_distinct (string_ord o pairself #1);
+      |> sort_distinct (string_ord o apply2 #1);
 
     fun enter ap1 sel2 entry =
       if SML <> exchange then