diff -r cce0570d1bfa -r 61a691db1c4d src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Tue Apr 05 15:53:48 2016 +0200
+++ b/src/Pure/ML/ml_file.ML	Tue Apr 05 15:58:58 2016 +0200
@@ -8,7 +8,7 @@
 sig
   val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
   val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
-  val any: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
+  val use: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure ML_File: ML_FILE =
@@ -32,7 +32,7 @@
 val ML = command (K false);
 val SML = command (K true);
 
-val any =
+val use =
   command (fn path =>
     (case try (#2 o Path.split_ext) path of
       SOME "ML" => false