--- a/src/Pure/pure_syn.ML Tue Mar 18 16:45:14 2014 +0100
+++ b/src/Pure/pure_syn.ML Tue Mar 18 17:39:03 2014 +0100
@@ -18,10 +18,10 @@
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