diff -r 0951d6cec68c -r 3c0f53eae166 src/Pure/ML/ml_compiler2.ML
--- a/src/Pure/ML/ml_compiler2.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Pure/ML/ml_compiler2.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -1,11 +1,11 @@
 (*  Title:      Pure/ML/ml_compiler2.ML
     Author:     Makarius
 
-Isabelle/ML use operations.
+Isabelle/ML file operations.
 *)
 
-val {use, use_debug, use_no_debug} =
-  ML_Compiler0.use_operations (fn opt_debug => fn file =>
+val {ML_file, ML_file_debug, ML_file_no_debug} =
+  ML_Compiler0.ML_file_operations (fn opt_debug => fn file =>
     let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in
       ML_Context.eval_file flags (Path.explode file)
         handle ERROR msg => (writeln msg; error "ML error")