diff -r 52d5067ca06a -r 06cc31dff138 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Tue Mar 18 16:45:14 2014 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Tue Mar 18 17:39:03 2014 +0100
@@ -12,7 +12,7 @@
     val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,
       {lines = fdl_lines, pos = fdl_pos, ...},
       {lines = rls_lines, pos = rls_pos, ...}], thy') = files thy;
-    val base = fst (Path.split_ext (File.full_path (Thy_Load.master_directory thy') src_path));
+    val base = fst (Path.split_ext (File.full_path (Resources.master_directory thy') src_path));
   in
     SPARK_VCs.set_vcs
       (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
@@ -24,7 +24,7 @@
 (* FIXME *)
 fun spark_open_old (vc_name, prfx) thy =
   let
-    val ((vc_path, vc_id), vc_text) = Thy_Load.load_file thy (Path.explode vc_name);
+    val ((vc_path, vc_id), vc_text) = Resources.load_file thy (Path.explode vc_name);
     val (base, header) =
       (case Path.split_ext vc_path of
         (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
@@ -117,13 +117,13 @@
 val _ =
   Outer_Syntax.command @{command_spec "spark_open_vcg"}
     "open a new SPARK environment and load a SPARK-generated .vcg file"
-    (Parse.parname -- Thy_Load.provide_parse_files "spark_open_vcg"
+    (Parse.parname -- Resources.provide_parse_files "spark_open_vcg"
       >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header));
 
 val _ =
   Outer_Syntax.command @{command_spec "spark_open_siv"}
     "open a new SPARK environment and load a SPARK-generated .siv file"
-    (Parse.parname -- Thy_Load.provide_parse_files "spark_open_siv"
+    (Parse.parname -- Resources.provide_parse_files "spark_open_siv"
       >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header));
 
 val pfun_type = Scan.option