src/Pure/Thy/thy_info.ML
changeset 58851 897f266c44b3
parent 58843 521cea5fa777
child 58852 621c052789b4
--- a/src/Pure/Thy/thy_info.ML	Fri Oct 31 21:10:11 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Oct 31 21:20:06 2014 +0100
@@ -14,7 +14,6 @@
   val get_theory: string -> theory
   val is_finished: string -> bool
   val master_directory: string -> Path.T
-  val loaded_files: string -> Path.T list
   val remove_thy: string -> unit
   val kill_thy: string -> unit
   val use_theories:
@@ -126,12 +125,6 @@
 
 val get_imports = Resources.imports_of o get_theory;
 
-(*Proof General legacy*)
-fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
-  (case get_deps name of
-    NONE => []
-  | SOME {master = (thy_path, _), ...} => thy_path :: Resources.loaded_files (get_theory name)));
-
 
 
 (** thy operations **)