--- 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