Thy_Info.loaded_files: Thy_Load.loaded_files depends on master -- i.e. no files for finished theory;
authorwenzelm
Mon, 26 Jul 2010 13:50:52 +0200
changeset 37955 f87d1105e181
parent 37954 a2e73df0b1e0
child 37956 ee939247b2fb
Thy_Info.loaded_files: Thy_Load.loaded_files depends on master -- i.e. no files for finished theory;
src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Jul 25 21:42:39 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Jul 26 13:50:52 2010 +0200
@@ -153,8 +153,10 @@
 fun loaded_files name =
   (case get_deps name of
     NONE => []
-  | SOME {master, ...} => (case master of SOME (thy_path, _) => [thy_path] | NONE => [])) @
-  Thy_Load.loaded_files (get_theory name);
+  | SOME {master, ...} =>
+      (case master of
+        NONE => []
+      | SOME (thy_path, _) => thy_path :: Thy_Load.loaded_files (get_theory name)));