src/Pure/ML/ml_file.ML

 Commands to load ML files.
 *)
 
 signature ML_FILE =
 sig
-  val command: string option -> bool option -> (theory -> Token.file list) ->
+  val command: string -> bool option -> (theory -> Token.file list) ->
     Toplevel.transition -> Toplevel.transition
   val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
   val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure ML_File: ML_FILE =
 struct
 
-fun command env debug files = Toplevel.generic_theory (fn gthy =>
+fun command environment debug files = Toplevel.generic_theory (fn gthy =>
   let
     val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     val provide = Resources.provide (src_path, digest);
     val source = Input.source true (cat_lines lines) (pos, pos);
 
     val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
 
     val flags: ML_Compiler.flags =
-      {read = env, write = env, redirect = true, verbose = true,
+      {environment = environment, redirect = true, verbose = true,
         debug = debug, writeln = writeln, warning = warning};
   in
     gthy
     |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
     |> Local_Theory.propagate_ml_env
     |> Context.mapping provide (Local_Theory.background_theory provide)
   end);
 
-val ML = command NONE;
-val SML = command (SOME ML_Env.SML);
+val ML = command "";
+val SML = command ML_Env.SML;
 
 end;