adapted ThyLoad.check_file etc.;
tuned signature;

--- a/src/Pure/Thy/present.ML	Thu Jul 19 23:18:55 2007 +0200
+++ b/src/Pure/Thy/present.ML	Thu Jul 19 23:18:56 2007 +0200
@@ -25,7 +25,7 @@
   val init_theory: string -> unit
   val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
   val theory_output: string -> string -> unit
-  val begin_theory: Path.T option -> string -> string list ->
+  val begin_theory: Path.T list -> string -> string list ->
     (Path.T * bool) list -> theory -> theory
   val add_hook: (string -> (string * thm list) list -> unit) -> unit
   val results: string -> (string * thm list) list -> unit
@@ -127,7 +127,7 @@
       else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
     unfold = false,
     parents =
-      map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}
+      map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_parents name)}
   end) (ThyInfo.names ());
 
 fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) =
@@ -452,16 +452,16 @@
        (html_path name))), name)
   end;
 
-fun begin_theory optpath name raw_parents orig_files thy =
+fun begin_theory dirs name raw_parents orig_files thy =
     with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
   let
     val parents = map (parent_link remote_path path) raw_parents;
     val ml_path = ThyLoad.ml_path name;
     val files = map (apsnd SOME) orig_files @
-      (if is_some (ThyLoad.check_file optpath ml_path) then [(ml_path, NONE)] else []);
+      (if is_some (ThyLoad.check_file dirs ml_path) then [(ml_path, NONE)] else []);
 
     fun prep_file (raw_path, loadit) =
-      (case ThyLoad.check_file optpath raw_path of
+      (case ThyLoad.check_ml dirs raw_path of
         SOME (path, _) =>
           let
             val base = Path.base path;