# HG changeset patch
# User wenzelm
# Date 1280145052 -7200
# Node ID f87d1105e181580667995416b3aa5f35c46ab21d
# Parent  a2e73df0b1e03c53cfc723da7181d63390f29b31
Thy_Info.loaded_files: Thy_Load.loaded_files depends on master -- i.e. no files for finished theory;

diff -r a2e73df0b1e0 -r f87d1105e181 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)));