src/Pure/pure_syn.ML

           (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
 
 val _ =
   Outer_Syntax.command
     (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
-    (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
+    (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
         let
           val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
-          val provide = Thy_Load.provide (src_path, digest);
+          val provide = Resources.provide (src_path, digest);
           val source = {delimited = true, text = cat_lines lines, pos = pos};
         in
           gthy
           |> ML_Context.exec (fn () => ML_Context.eval_source true source)
           |> Local_Theory.propagate_ml_env