tuned signature;

--- a/src/Pure/Thy/thy_info.ML	Sat Nov 16 13:07:38 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Nov 16 13:12:02 2013 +0100
@@ -126,6 +126,7 @@
 
 val get_imports = Thy_Load.imports_of o get_theory;
 
+(*Proof General legacy*)
 fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   (case get_deps name of
     NONE => []
@@ -305,7 +306,7 @@
           #2 master = #2 master' andalso
             (case lookup_theory name of
               NONE => false
-            | SOME theory => Thy_Load.load_current theory);
+            | SOME theory => Thy_Load.loaded_files_current theory);
       in (current, deps', theory_pos', imports', keywords') end);
 
 in

--- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 13:07:38 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 13:12:02 2013 +0100
@@ -18,7 +18,7 @@
   val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
   val use_file: Path.T -> theory -> string * theory
   val loaded_files: theory -> Path.T list
-  val load_current: theory -> bool
+  val loaded_files_current: theory -> bool
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -170,11 +170,12 @@
     val thy' = provide (src_path, id) thy;
   in (text, thy') end;
 
+(*Proof General legacy*)
 fun loaded_files thy =
   let val {master_dir, provided, ...} = Files.get thy
   in map (File.full_path master_dir o #1) provided end;
 
-fun load_current thy =
+fun loaded_files_current thy =
   #provided (Files.get thy) |>
     forall (fn (src_path, id) =>
       (case try (load_file thy) src_path of