# HG changeset patch
# User wenzelm
# Date 1313873179 -7200
# Node ID d453faed48158e563987aa68cc5781c91ae7d26b
# Parent  59ff5a93eef489c402c155dc88d36852928ac754
clarified get_imports -- should not rely on accidental order within graph;

diff -r 59ff5a93eef4 -r d453faed4815 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Aug 20 22:28:53 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Aug 20 22:46:19 2011 +0200
@@ -113,10 +113,6 @@
 val is_finished = is_none o get_deps;
 val master_directory = master_dir o get_deps;
 
-fun get_parents name =
-  thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
-    error (loader_msg "nothing known about theory" [name]);
-
 
 (* access theory *)
 
@@ -130,6 +126,8 @@
     SOME theory => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
+val get_imports = Thy_Load.imports_of o get_theory;
+
 fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   (case get_deps name of
     NONE => []
@@ -242,7 +240,7 @@
 
 fun check_deps dir name =
   (case lookup_deps name of
-    SOME NONE => (true, NONE, get_parents name)
+    SOME NONE => (true, NONE, get_imports name)
   | NONE =>
       let val {master, text, imports, ...} = Thy_Load.check_thy dir name
       in (false, SOME (make_deps master imports, text), imports) end