--- 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