src/Pure/Thy/thy_load.ML

 (* load files *)
 
 fun load_ml dir raw_path =
   (case check_ml dir raw_path of
     NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
-  | SOME (path, id) => (ML_Context.use path; (path, id)));
+  | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
 
 (*dependent on outer syntax*)
 val load_thy_fn =
   ref (undefined: Path.T -> string -> Position.T -> string list -> bool -> unit);
 fun load_thy dir name pos text time = ! load_thy_fn dir name pos text time;